Theorem negsym1

Description: In the paper "On Variable Functors of Propositional Arguments", Lukasiewicz introduced a system that can handle variable connectives. This was done by introducing a variable, marked with a lowercase delta, which takes a wff as input. In the system, "delta ph " means that "something is true of ph ". The expression "delta ph " can be substituted with -. ph , ps /\ ph , A. x ph , etc.

Later on, Meredith discovered a single axiom, in the form of ( delta delta F. -> delta ph ) . This represents the shortest theorem in the extended propositional calculus that cannot be derived as an instance of a theorem in propositional calculus.

A symmetry with -. . (Contributed by Anthony Hart, 4-Sep-2011)

	Ref	Expression
Assertion	negsym1	⊢ ( ¬ ¬ ⊥ → ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		fal	⊢ ¬ ⊥
2	1	pm2.24i	⊢ ( ¬ ¬ ⊥ → ¬ 𝜑 )