Commit cbc68180 authored by jfschaefer's avatar jfschaefer

added PLNQ stuff from lecture

parent 11a672bd
namespace http://mathhub.info/lbs1920/plnq ❚
// Theory for predicate logic without quantifiers (PLNQ) ❚
theory PLNQ : ur:?LF =
// A type for propositions ❙
prop : type ❙
// Conjunction (AND) is a function that takes two propositions and creates a new one ❙
// We introduce a notation for it: The wedge (∧) ❙
// We also set a precedence to make it bind e.g. weaker than negation ❙
conjunction : prop ⟶ prop ⟶ prop ❘ # 1 ∧ 2 prec 60❙
negation : prop ⟶ prop ❘ # ¬ 1 prec 80 ❙
disjunction : prop ⟶ prop ⟶ prop ❘ # 1 ∨ 2 prec 50 ❘ = [A,B] ¬ ( ¬ A ∧ ¬ B ) ❙
implication : prop ⟶ prop ⟶ prop ❘ # 1 ⇒ 2 prec 40 ❘ = [A,B] ¬ A ∨ B ❙
biimplication : prop ⟶ prop ⟶ prop ❘ # 1 ⇔ 2 prec 30 ❙
// Judgements ("it holds that") ❙
// They are used to state that a particular proposition is true ❙
// From a technical point of view, ⊢ A is the type of all proves of A ❙
// So when we declare x : ⊢ A, we state that x is a proof of A, i.e. A is true/an axiom ❙
ded : prop ⟶ type ❘ # ⊢ 1 prec 10❙
// Proof rules ❙
// For propositions A and B,
andIntroduction transforms a proof of A and a proof of B into a proof of A ∧ B ❙
andIntroduction : {A, B} ⊢ A ⟶ ⊢ B ⟶ ⊢ (A ∧ B) ❘ # andI 3 4 ❙
andEliminationLeft : {A, B} ⊢ (A ∧ B) ⟶ ⊢ B ❘ # andEl 3 ❙
// ⊢ (A ∧ B) is the type of proofs for A ∧ B ❙
andEliminationRight : {A, B} ⊢ (A ∧ B) ⟶ ⊢ A ❘ # andEr 3 ❙
implicationIntroduction : {A,B} (⊢ A ⟶ ⊢ B) ⟶ ⊢ (A ⇒ B) ❘ # implI 3 ❙
// Proof that A ∧ B ⇒ B ∧ A given any A and B ❙
andCommutativity : {A, B} ⊢ (A ∧ B ⇒ B ∧ A) ❘ =
[A, B] implI ([p : ⊢ A ∧ B] (andI (andEl p) (andEr p))) ❘ # andC 1 2 ❙
// Some example propositions ❙
johnlovesmary : prop ❘ # jlm ❙
gabisleeps : prop ❘ # gs ❙
// theorem (because we have a proof) ❙
test : ⊢ jlm ∧ gs ⇒ gs ∧ jlm ❘ = andC jlm gs❙
// axioms (no proof) ❙
s1 : ⊢ johnlovesmary ❙
s2 : ⊢ gabisleeps ❙
// proof (of a theorem) using axioms ❙
proof : ⊢ jlm ∧ gs ❘ = andI s1 s2 ❙
theory WorldBase : ?PLNQ =
Person : type ❙
peter : Person ❙
gabi : Person ❙
mary : Person ❙
predicate1 : type ❘ = Person ⟶ prop ❘ # p1 ❙
sleep : p1 ❙
predicate2 : type ❘ = Person ⟶ p1 ❘ # p2 ❙
love : p2 ❙
// "Peter loves Mary" ❙
sentence1 : prop ❘ = love peter mary ❙
// "Gabi sleeps" ❙
sentence2 : prop ❘ = sleep gabi ❙
// "Peter loves Mary and Gabi sleeps" ❙
sentence3 : prop ❘ = sentence1 ∧ sentence2 ❙
theory World1 : ?PLNQ =
include ?WorldBase ❙
// "sentence1 is actually true" ❙
s1holds = ⊢ sentence1 ❙
theory World2 : ?PLNQ =
include ?WorldBase ❙
// "sentence1 is false" ❙
s1holds = ⊢ ¬ sentence1 ❙
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment