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.

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.