# Proof for "⊢ (A → ¬¬A)"

I've spent 4.5 hours on this, with no exaggeration. I clearly have no idea what I'm doing here, and it's become a serious time sink. If any of you could help in proving this, I would be eternally grateful. I learn best by examining correct responses and applying the concepts forwards, and without that sort of support on this question, I'm ready to start slamming my head into things.

• Assume ¬A and derive a contradiction with premise A. Commented Feb 15, 2022 at 7:22

I am new to proof. Does this work?

• This works even in intuitionistic logic! Note in IL ¬¬A⊬A due to double negation invocation otherwise, but the above direction is still valid... Commented Feb 23, 2022 at 6:34

What was your motivation to spend that time looking at this problem? In my fantasy, you were trying to taste the flavor of proving a mathematical result.

There are two ways to proof this type of statement in a mathematical sense:

• To use a truth table, which is an algorithm that decides if a sentence of this type is true or not. This is easy: if "T" and "F" designate true and false, T=not not T and F=not not F. This doesn't look like a cool proof. By the way this algorithm was discovered by the great Wittgenstein. That discovery had a strong impact on the Tractatus.

• To derive it from a set of axioms. These are several sentences that are true according to the truth table. In general we choose short sentences. The derivations are very technical and are not intuitive at all. The set of sentences we fix as axioms is more or less arbitrary. It should be smaller and the statements should look obvious. This last criteria is not always fulfilled.

I would say that it is hard to get that feeling of accomplishment from proving a tautology. If you or some other member of this group is interested on that, I would advice to learn how to make a proof by induction, assuming Peano's axioms. There you are really doing maths. Propositional Calculus is not the real thing (there is no mystery there, Godel's argument doesn't apply).

The proof might be said to be hard if it is required to be done in Hilbert-style. So, I take the question implying such a derivation. For a proof, see my post in which the theorem occurs in line 23.