Users' Mathboxes Mathbox for Anthony Hart < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  negsym1 Unicode version

Theorem negsym1 24196
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." "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.)

Assertion
Ref Expression
negsym1  |-  ( -. 
-.  F.  ->  -.  ph )

Proof of Theorem negsym1
StepHypRef Expression
1 fal 1319 . 2  |-  -.  F.
21pm2.24i 138 1  |-  ( -. 
-.  F.  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    F. wfal 1313
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-tru 1315  df-fal 1316
  Copyright terms: Public domain W3C validator