# Syllogism is a tautology

## Description

It's the first step that we define propositional logic (as deep embedding) when we use a novel prover, isn't it?

In Agda, it is easy to define propositions and an evaluation function with valuation function.

After the definition, we would define inference rules for the logic, and verify them.

Here, we just test the evaluation function by checking results for tautologies, for instance, modus-ponens and syllogism.

We already use modus-ponens in Agda challenge, so let's prove syllogism is a tautology.

The definition of propositions is very redundant (for this problem), but the redundancy does not affect a proof.

## Definitions (download)

module Definitions where open import Data.Bool open import Data.Nat data Form : Set where ⊥ : Form _⊃_ : Form -> Form -> Form Atom : ℕ -> Form ev : Form -> (ℕ -> Bool) -> Bool ev ⊥ φ = false ev (P ⊃ Q) φ = not (ev P φ) ∨ ev Q φ ev (Atom m) φ = φ m data _==_ {A : Set} (x : A) : A -> Set where refl : x == x tauto : Form -> Set tauto P = ∀ φ -> ev P φ == true

## Theorem (download)

module Theorem where open import Definitions postulate syllogism-is-tauto : (P Q R : Form) -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)))

## Verifier

module Verifier where open import Definitions open import Theorem verify : (P Q R : Form) -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R))) verify = syllogism-is-tauto

## Proofs

Rank | Prover | Size | Date |
---|---|---|---|

1 | strout | 245 | 2014-01-06 12:19:46 JST |

2 | phi16_ | 294 | 2017-11-14 15:57:33 JST |

3 | trigott | 323 | 2014-04-16 00:16:16 JST |

4 | kiritex | 323 | 2014-04-04 17:59:00 JST |

5 | Rotsor | 344 | 2013-12-28 23:44:23 JST |

6 | notogawa | 351 | 2013-05-29 22:37:58 JST |

7 | masahiro_sakai | 368 | 2014-11-25 23:32:40 JST |

8 | chiguri | 728 | 2013-05-29 18:03:08 JST |

9 | kdxu | 739 | 2014-03-16 16:59:30 JST |

10 | nrolland | 1060 | 2014-12-26 03:59:23 JST |