Are Logicians Naturally Logical?


Natural Logic (with modus ponens additives)

Implication: p->q->r for (p->q)->r
p -> (q->p); p->(q->r) -> (p->q -> (p->r))
Theorems: p -> p
Deduction theorem (natural deduction); Substitution theorem

Conjunction, Disjunction
p -> (q -> pq); pq -> p; pq -> q
p -> pvq; q -> pvq; p->r -> (q->r -> (pvq -> r))
Theorems
pq <-> qp; pvq <-> qvp; p(qr) <-> (pq)r; pv(qvr) <-> (pvq)vr
pp <-> p; pvp <-> p; p <-> p v pq; p <-> p(pvq)
p(qvr) <-> pq v pr; (pvq)(pvr) <-> p v qr
(p<->q) <-> (pr<->qr)(pvr<->qvr)

Quantifiers
Ax.p(x) -> p(t); p(t) -> Ex.p(x), if t substitutable for x
Ax(p->q) -> (Ax.p -> Ax.q)(Ex.p -> Ex.q)
Ex.p -> p; p -> Ax.p, if no free x in p
rule G: If p1,..pk |- q, no free x in p1,..pk, then p1,..pk |- Ax.q
rule C: If p1,..pk q(x) |- r, no free x in p1,..pk,r
then p1,..pk, Ex.q(x) |- r

* * * So what are Ax, Ex introduction and elimination rules? * * *

Positive Logic: p->q->p -> p, Pierce's axiom
Natural Negation: ~p =df p->f
Intitutionistic Negation: f -> p
Classical Negation: ~~p -> p

----
.

Relevant Pages

  • Re: good examples of scary encounters?
    ... > more than a few theorems that way. ... Well, as I said to Patricia, it's not so much the explaining--I've been ... "I never understood people who don't have bookshelves." ... Prev by Date: ...
    (rec.arts.sf.composition)
  • Re: good examples of scary encounters?
    ... Clears the mind wonderfully; I've proved ... more than a few theorems that way. ... Brian ... Prev by Date: ...
    (rec.arts.sf.composition)
  • p-adic transcendental numbers
    ... Many theorems have been proved giving sufficient conditions ... Prev by Date: ...
    (sci.math)
  • Re: Another recursion theory / decidability question
    ... the set of theorems one can prove using S as a ... International Symposium at Berkeley. ... --Herb Enderton ... Prev by Date: ...
    (sci.logic)
  • Compute |E:Q||
    ... I don't know what it is with these but I don't see any theorems that ... allow me to easily know how to copute this. ... I'm clueless as to how to proceed on 2. ... Prev by Date: ...
    (sci.math)
Quantcast