Re: [isabelle] I want to print axiomatization info
On 7/10/2012 2:14 AM, Lars Noschinski wrote:
So I reduce (!R. ((P --> Q --> R) --> R)) down to
!R. ((P /\ Q) \/ R)
This would be "!R. (~(P /\ Q) \/ R)"
I don't know. This is what I get:
(P --> Q --> R) --> R
== ((P /\ Q) --> R) --> R)
== (~(P /\ Q) \/ R) --> R)
== ~(~(P /\ Q) \/ R) \/ R
== ((P /\ Q) /\ ~R) \/ R
== ((P /\ Q) \/ R) /\ (~R \/ 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.
Okay, that's good to know. I'm still transitioning from truth tables,
where writing a formula doesn't assert anything, at least that's how
I've always viewed it for the connectives /\, \/, -->, and ~.
I did decide previously that I should interpret "!P. P" as asserting
that P is always true, which helps me with it being the definition of
False, but it doesn't help me understand
!R. ((P /\ Q) \/ R), or even
!R. (~(P /\ Q) \/ R).
The "P" and "Q" part of the "conj" (infixed as "&", and "/\") definition
makes sense to me because when I use the function
conj P Q,
in my mind, I go through the truth table and make assignments to "P" and
"Q" and decide what result I should get based on how the function was
being used in a statement.
!R. ((P /\ Q) \/ R),
I try to use the same trick and say, "it's asserting that for every R, R
is always true", but that doesn't work. If R is always true, then the
statement is always true. But if it's always false, then the statement
operates as a conjunction.
Well, okay, the above sentence shows I still have trouble interpreting
What I know is that saying "every proposition R is true" is a false
statement, so if that's what makes R always false in the statement "((P
/\ Q) \/ R)", then the statement as a whole works.
Ah, maybe I have it. The statement "!R. ((P /\ Q) \/ R)" could be
"For every proposition R, (P /\ Q) is true or R is true."
A more friendlier statement would be this, using your statement above:
"Every proposition is true or (P /\ Q) is true".
I guess that's it. Simple stuff, unless it's not.
Thanks for the help.
This archive was generated by a fusion of
Pipermail (Mailman edition) and