From 48167a7aee5f5fbac6761468d0e59fb3d97020cf Mon Sep 17 00:00:00 2001 From: Landon D. C. Elkind Date: Wed, 3 Feb 2021 16:04:24 -0700 Subject: PL prettified further --- PL.pdf | Bin 436367 -> 420430 bytes PL.v | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/PL.pdf b/PL.pdf index 57914c0..7fe64e3 100644 Binary files a/PL.pdf and b/PL.pdf differ diff --git a/PL.v b/PL.v index 9809b74..687fd9b 100644 --- a/PL.v +++ b/PL.v @@ -15,7 +15,7 @@ Axiom Impl1_01 : ∀ P Q : Prop, Axiom MP1_1 : ∀ P Q : Prop, (P → Q) → P → Q. (*Modus ponens*) - (**1.11 ommitted: it is MP for propositions + (*1.11 ommitted: it is MP for propositions containing variables. Likewise, ommitted the well-formedness rules 1.7, 1.71, 1.72*) -- cgit v1.2.3