On 4/11/2017 9:21 AM, David Nyman wrote:

    Yet, if the current theory is the giving of the two axioms:

    A1   p -> (q -> p)
    A2   (p -> (q -> r) )  ->  ((p -> q) -> (p -> r))

    With the inference rules modus ponens, and some substitution rule,
     it will be rather difficult to find a proof of (p -> p).

    But here, all what the man in the street is asked is in 1)
    understanding that this is difficult, and 2) being able to verify
    if a proof is indeed a proof, that is, a sequence of formula which
    starts from some axiom, and use only axiom, or formula derived
    from the axioms using only the given inference rule. Even that can
    be very complex, and usually we add comment to help (like the
    comment in a program).


​ Yes, this is important. Failing to do this, even in informal reasoning,​ leads directly to question begging, as I'm fond of pointing out. All the more pernicious when (as is usual) the smuggling in of auxiliary assumptions is almost always tacit and unrecognised.


    Here is a proof of (p -> p):


But why choose A1 and A2? Why not make (p -> p) and axiom. It's certainly more obvious than either A1 of A2, so if it were not a theorem you'd got back choose different axioms. Actually I know why; but my point is that logic is intended to formalize sound inference - but because it's formal it is only "t" preserving, not truth preserving.

Brent

--
You received this message because you are subscribed to the Google Groups 
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.

Reply via email to