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