Gustavo Bandeira (Mar 18 2024 at 06:10): Gustavo Bandeira (Mar 18 2024 at 06:10):If A is true, we use the following Hilbert axiom A->(B->A) with A=B and Modus Ponens, then we get A->A?
Jonathan Julian Huerta y Munive (Mar 18 2024 at 09:34):If I remember correctly, this is a valid argument in Hilbert's axiom system and one of the first proofs that one does. You could take a look at Introduction to Mathematical Logic by Elliott Mendelson to double check, and I also would recommend that you focus on Isabelle related questions, and check if people have asked something similar before.
Last updated: Apr 27 2024 at 20:14 UTC