From 610ac0e2ef212636ce5dabd108c3ba2e2b14fc49 Mon Sep 17 00:00:00 2001
From: Landon D. C. Elkind
Date: Wed, 3 Feb 2021 16:05:11 -0700
Subject: Delete No1.v

---
 No1.v | 30 ------------------------------
 1 file changed, 30 deletions(-)
 delete mode 100644 No1.v

diff --git a/No1.v b/No1.v
deleted file mode 100644
index 6652c03..0000000
--- a/No1.v
+++ /dev/null
@@ -1,30 +0,0 @@
-Require Import Unicode.Utf8.
-
-Module No1. 
-
-Import Unicode.Utf8. (*We first give the axioms of Principia for the propositional calculus in *1.*)
-
-Axiom MP1_1 : ∀  P Q : Prop,
-  (P → Q) → P → Q. (*Modus ponens*)
-
-  (**1.11 ommitted: it is MP for propositions containing variables. Likewise, ommitted the well-formedness rules 1.7, 1.71, 1.72*)
-
-Axiom Taut1_2 : ∀ P : Prop, 
-  P ∨ P→ P. (*Tautology*)
-
-Axiom Add1_3 : ∀ P Q : Prop, 
-  Q → P ∨ Q. (*Addition*)
-
-Axiom Perm1_4 : ∀ P Q : Prop, 
-  P ∨ Q → Q ∨ P. (*Permutation*)
-
-Axiom Assoc1_5 : ∀ P Q R : Prop, 
-  P ∨ (Q ∨ R) → Q ∨ (P ∨ R).
-
-Axiom Sum1_6: ∀ P Q R : Prop, 
-  (Q → R) → (P ∨ Q → P ∨ R). (*These are all the propositional axioms of Principia Mathematica.*)
-
-Axiom Impl1_01 : ∀ P Q : Prop, 
-  (P → Q) = (~P ∨ Q). (*This is a definition in Principia: there → is a defined sign and ∨, ~ are primitive ones. So we will use this axiom to switch between disjunction and implication.*)
-
-End No1.
\ No newline at end of file
-- 
cgit v1.2.3