逻辑是一切思考的基础。

# Propositional logic(zeroth order logic)

Propositional logic does NOT deal with non-logical objects, predicates or quantifiers.

For example, the following simple axiom system is an instance of propositional logic:

L(A,Ω,Z,I)\mathcal{L}(A,\Omega,Z,I):

  • A={p,q,r,s,t,...}A=\{p,q,r,s,t,...\} serves to represent logic propositions.

  • Ω={¬,→}\Omega=\{\neg,\rightarrow\} is the set of logic operators.

  • ZZ is the set of transformation rule. Here it contains only one rule named modus ponens:

    p→q,p⊢qp\rightarrow q,p\vdash q

  • II is the set of axioms. The axioms are all substitution instances of:

    ⊢p→(q→p)⊢(p→(q→r))→((p→q)→(p→r))⊢(¬p→¬q)→(q→p)\begin{aligned} &\vdash p\rightarrow(q\rightarrow p)\\ &\vdash (p\rightarrow(q\rightarrow r))\rightarrow((p\rightarrow q)\rightarrow(p\rightarrow r))\\ &\vdash (\neg p\rightarrow\neg q)\rightarrow(q\rightarrow p) \end{aligned}

Example: the proof of ¬¬p⊢p\neg\neg p\vdash p:

  • Lemma 1. ⊢p→p\vdash p\rightarrow p.

    Proof.

    (1) By axiom 1, substitute qq with p→pp\rightarrow p, we have

    p→((p→p)→p)p\rightarrow((p\rightarrow p)\rightarrow p)

    (2) By axiom 2, substitute qq with p→pp\rightarrow p and substitute rr with pp:

    (p→((p→p)→p)→((p→(p→p))→(p→p))(p\rightarrow((p\rightarrow p)\rightarrow p)\rightarrow((p\rightarrow(p\rightarrow p))\rightarrow (p\rightarrow p))

    (3) By Modus ponens and (1), (2):

    (p→(p→p))→(p→p)(p\rightarrow(p\rightarrow p))\rightarrow(p\rightarrow p)

    (4) By axiom 1, substitute qq with pp:

    p→(p→p)p\rightarrow(p\rightarrow p)

    (5) By Modus ponens and (3), (4):

    p→pp\rightarrow p

  • Lemma 2. p→q,q→r⊢p→rp\rightarrow q,q\rightarrow r\vdash p\rightarrow r.

    Proof.

    (1) p→qp\rightarrow q premise

    (2) q→rq\rightarrow r premise

    (3) By axiom 1,

    (q→r)→(p→(q→r))(q\rightarrow r)\rightarrow(p\rightarrow(q\rightarrow r))

    (4) By Modus ponens and (2), (3):

    p→(q→r)p\rightarrow (q\rightarrow r)

    (5) By axiom 2,

    (p→(q→r))→((p→q)→(p→r))(p\rightarrow(q\rightarrow r))\rightarrow((p\rightarrow q)\rightarrow(p\rightarrow r))

    (6) By Modus ponens and (4), (5):

    (p→q)→(p→r)(p\rightarrow q)\rightarrow(p\rightarrow r)

    (7) By Modus ponens and (1), (6):

    p→rp\rightarrow r

  • Lemma 3. (q→r)→((p→q)→(p→r))(q\rightarrow r)\rightarrow((p\rightarrow q)\rightarrow(p\rightarrow r)).

    Proof.

    (1) By axiom 1, substitute pp with (p→(q→r))→((p→q)→(p→r))(p\rightarrow (q\rightarrow r))\rightarrow ((p\rightarrow q)\rightarrow (p\rightarrow r)),

    ((p→(q→r))→((p→q)→(p→r)))→([q→r]→((p→(q→r))→((p→q)→(p→r))))((p\rightarrow (q\rightarrow r))\rightarrow ((p\rightarrow q)\rightarrow (p\rightarrow r)))\rightarrow ([q\rightarrow r]\rightarrow ((p\rightarrow (q\rightarrow r))\rightarrow ((p\rightarrow q)\rightarrow (p\rightarrow r))))

    (2) By axiom 2,

    (p→(q→r))→((p→q)→(p→r))(p\rightarrow (q\rightarrow r))\rightarrow ((p\rightarrow q)\rightarrow (p\rightarrow r))

    (3) By Modus ponens and (1), (2),

    (q→r)→((p→(q→r))→((p→q)→(p→r)))(q\rightarrow r)\rightarrow ((p\rightarrow (q\rightarrow r))\rightarrow ((p\rightarrow q)\rightarrow (p\rightarrow r)))

    (4) By axiom 2,

    [(q→r)→((p→(q→r))→((p→q)→(p→r)))]→[(q→r)→(p→(q→r))→((q→r)→((p→q)→(p→r)))][(q\rightarrow r)\rightarrow ((p\rightarrow (q\rightarrow r))\rightarrow ((p\rightarrow q)\rightarrow (p\rightarrow r)))]\rightarrow[(q\rightarrow r)\rightarrow(p\rightarrow(q\rightarrow r))\rightarrow ((q\rightarrow r)\rightarrow ((p\rightarrow q)\rightarrow(p\rightarrow r)))]

    (5) By Modus ponens and (3) (4),

    [(q→r)→(p→(q→r))]→((q→r)→((p→q)→(p→r)))[(q\rightarrow r)\rightarrow (p\rightarrow(q\rightarrow r))]\rightarrow ((q\rightarrow r)\rightarrow((p\rightarrow q)\rightarrow(p\rightarrow r)))

    (6) By axiom 1,

    (q→r)→(p→(q→r))(q\rightarrow r)\rightarrow(p\rightarrow(q\rightarrow r))

    (7) By Modus ponens and (5), (6),

    (q→r)→((p→q)→(p→r))(q\rightarrow r)\rightarrow((p\rightarrow q)\rightarrow(p\rightarrow r))

  • Lemma 4. ⊢p→((p→q)→q)\vdash p\rightarrow((p\rightarrow q)\rightarrow q).

    Proof.

    (1) By axiom 3,

    ((p→q)→(p→q))→(((p→q)→p)→((p→q)→q))((p\rightarrow q)\rightarrow(p\rightarrow q))\rightarrow(((p\rightarrow q)\rightarrow p)\rightarrow((p\rightarrow q)\rightarrow q))

    (2) By Lemma 1,

    (p→q)→(p→q)(p\rightarrow q)\rightarrow(p\rightarrow q)

    (3) By Modus ponens and (1) (2),

    ((p→q)→p)→((p→q)→q)((p\rightarrow q)\rightarrow p)\rightarrow((p\rightarrow q)\rightarrow q)

    (4) By Lemma 3,

    (((p→q)→p)→((p→q)→q))→((p→((p→q)→p))→(p→((p→q)→q)))(((p\rightarrow q)\rightarrow p)\rightarrow((p\rightarrow q)\rightarrow q))\rightarrow ((p\rightarrow ((p\rightarrow q)\rightarrow p))\rightarrow (p\rightarrow ((p\rightarrow q)\rightarrow q)))

    (5) By Modus ponens and (3) (4),

    (p→((p→q)→p))→(p→((p→q)→q))(p\rightarrow((p\rightarrow q)\rightarrow p))\rightarrow (p\rightarrow ((p\rightarrow q)\rightarrow q))

    (6) By axiom 1,

    p→((p→q)→p)p\rightarrow ((p\rightarrow q)\rightarrow p)

    (7) By Modus ponens, (5) (6),

    p→((p→q)→q)p\rightarrow((p\rightarrow q)\rightarrow q)

  • Proposition ⊢¬¬p→p\vdash \neg\neg p\rightarrow p.

    Proof.

    (1) By axiom 1, ϕ::=(r→(s→t))\phi::=(r\rightarrow (s\rightarrow t)).

    (2) By axiom 3,

    (¬¬ϕ→¬¬p)→(¬p→¬ϕ)(\neg\neg\phi\rightarrow \neg\neg p)\rightarrow(\neg p\rightarrow \neg \phi)

    (3) By axiom 3,

    (¬p→¬ϕ)→(ϕ→p)(\neg p\rightarrow\neg \phi)\rightarrow(\phi\rightarrow p)

    (4) By axiom 1,

    ¬¬p→(¬¬ϕ→¬¬p)\neg\neg p\rightarrow(\neg\neg\phi\rightarrow\neg\neg p)

    (5) By Modus ponens, (3)(4),

    ¬¬p→(ϕ→p)\neg\neg p\rightarrow(\phi\rightarrow p)

    (6) By Lemma 4,

    ϕ→((ϕ→p)→p)\phi\rightarrow((\phi\rightarrow p)\rightarrow p)

    (7) By axiom 1,

    ϕ\phi

    (8) By Modus ponens, (6), (7),

    (ϕ→p)→p(\phi\rightarrow p)\rightarrow p

    (9) By Lemma 2, (5), (8),

    ¬¬p→p\neg\neg p\rightarrow p

□\square.

# First-order logic

Consider such an example, there are two propositions:

  1. John is male.
  2. Mike is male.

In propositional logic, we could only to describe with two symbols, that is:

p=John is maleq=Mike is malep=\text{John is male}\\ q=\text{Mike is male}

But “is male” seems to be duplicated part, so we develop a new logic system with predicate and variables.

Let P(x)=x is maleP(x)=\text{x is male}, and the two propositions could be interpreted as P(John)P(\text{John}) and P(Mike)P(\text{Mike}).


First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as “Socrates is a man”, one can have expressions in the form “there exists x such that x is Socrates and x is a man”, where “there exists*”* is a quantifier, while x is a variable.[1] This distinguishes it from propositional logic, which does not use quantifiers or relations;[2] in this sense, propositional logic is the foundation of first-order logic.

For example, the following formula is a proposition of first order logic

∀x∀y(P(f(x)))→¬(P(x)→Q(f(x),x,z)))\forall x\forall y(P(f(x)))\rightarrow\neg(P(x)\rightarrow Q(f(x),x,z)))

# Second/Higher order logic

First-order logic can quantify over individuals, but not over properties. But in Higher order logic, the following proposition is legitimate:

∀x∀P(P(x))\forall x\forall P(P(x))

while it’s forbidden in first order logic to ∀P\forall P since PP is a predicate.

In higher order logic, you could almost quantifier over any thing, that is

∀f,∃f\forall f,\exists f

where ff is a function, or predicate, or variables…

編集日 閲覧数 回