Definition. We define False to be ∀p : prop, p of type prop.
In Proofgold the corresponding term root is 1db705... and object id is 266ad5...
L1
Definition. We define not to be λA : prop ⇒ A → False of type prop → prop.
In Proofgold the corresponding term root is f30435... and object id is 0dc3c7...
Notation. We use ¬ as a prefix operator with priority 700 corresponding to applying term not.
L6
Definition. We define and to be λA B : prop ⇒ ∀p : prop, (A → B → p) → p of type prop → prop → prop.
In Proofgold the corresponding term root is 2ba7d0... and object id is 37da83...
Notation. We use ∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term and.
L11
Definition. We define or to be λA B : prop ⇒ ∀p : prop, (A → p) → (B → p) → p of type prop → prop → prop.
In Proofgold the corresponding term root is 957746... and object id is 86ae64...
Notation. We use ∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term or.
Beginning of Section Eq
L18
Variable A : SType
L19
Definition. We define eq to be λx y : A ⇒ ∀Q : A → A → prop, Qxy → Qyx of type A → A → prop.
L20
Definition. We define neq to be λx y : A ⇒ ¬eqxy of type A → A → prop.
End of Section Eq
Notation. We use = as an infix operator with priority 502 and no associativity corresponding to applying term eq.
Notation. We use ≠ as an infix operator with priority 502 and no associativity corresponding to applying term neq.
Beginning of Section Ex
L28
Variable A : SType
L29
Definition. We define ex to be λQ : A → prop ⇒ ∀P : prop, (∀x : A, Qx → P) → P of type (A → prop) → prop.
End of Section Ex
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex.
Primitive. The name In is a term of type set → set → prop.
Notation. We use ∈ as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write ∀ x ∈ A, B to mean ∀ x : set, x ∈ A → B.
L36
Definition. We define Subq to be λA B ⇒ ∀x ∈ A, x∈B of type set → set → prop.
In Proofgold the corresponding term root is 81c0ef... and object id is 317007...
Notation. We use ⊆ as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write ∀ x ⊆ A, B to mean ∀ x : set, x ⊆ A → B.
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex and handling ∈ or ⊆ ascriptions using and.
Primitive. The name 𝒫 is a term of type set → set.
Primitive. The name ordsucc is a term of type set → set.
In Proofgold the corresponding term root is 65d883... and object id is 1452f7...
Notation. Natural numbers 0,1,2,... are notation for the terms formed using Empty as 0 and forming successors with ordsucc.
L50
Definition. We define bij to be λX Y f ⇒ (∀u ∈ X, fu∈Y)∧(∀u v ∈ X, fu=fv → u=v)∧(∀w ∈ Y, ∃u ∈ X, fu=w) of type set → set → (set → set) → prop.
In Proofgold the corresponding term root is 76bef6... and object id is f7d93b...
L58
Definition. We define equip to be λX Y : set ⇒ ∃f : set → set, bijXYf of type set → set → prop.
In Proofgold the corresponding term root is eb4419... and object id is 7f2bf6...
L61
Definition. We define TwoRamseyProp to be λM N V ⇒ ∀R : set → set → prop, (∀x y, Rxy → Ryx) → ((∃X ⊆ V, equipMX∧(∀x y ∈ X, x≠y → Rxy))∨(∃Y ⊆ V, equipNY∧(∀x y ∈ Y, x≠y → ¬Rxy))) of type set → set → set → prop.
In Proofgold the corresponding term root is c5d86c... and object id is faf73f...