Re: [isabelle] I want to print axiomatization info
On 10.07.2012 02:42, Gottfried Barrow wrote:
On 7/9/2012 2:35 PM, Lawrence Paulson wrote:
I honestly don't think doing such substitutions is of any benefit at all.
See if you can make some sense of each definition individually.
I can make sense of the logic with these equivalencies:
(A --> B --> C) == ((A /\ B) --> C), and
(A --> B) == (~A \/ B).
So I reduce (!R. ((P --> Q --> R) --> R)) down to
!R. ((P /\ Q) \/ R)
This would be "!R. (~(P /\ Q) \/ R)"
So when R=false, the reduction above functions like conjunction. This
brings to my attention to the definition
False == (!P. P).
"!P. P" just says "all propositions hold". As long as our logic is
consistent, this is not going to be the case, so we choose this as our
value for False.
This archive was generated by a fusion of
Pipermail (Mailman edition) and