The Theory pcf-axs
Parents
pcf-defs
Constants
$∈c
PC → PC → BOOL
Fixity
Right Infix 300:
c
Axioms
pc_ext
⊢ ∀ c1 c2• c1 = c2 ⇔ (∀ f• f ∈f c1 ⇔ f ∈f c2)
pf_ext
⊢ ∀ f1 f2
fill• f1 = f2
fill⇔ domc f1 = domc f2
fill∧ codc f1 = codc f2
fill∧ (∀ f• f ∈f domc f1 ⇒ f1 f f = f2 f f)
associative_axiom
⊢ ∀ f g h
fill• codc h = domc g ∧ codc g = domc f
fill⇒ f of g of h = (f of g) of h
identity_axiom
⊢ ∀ c f
fill• (domc f = c ⇒ idf c of f = f)
fill∧ (codc f = c ⇒ f of idf c = f)
pc_closure_axiom
⊢ ∀ c f g
fill• f ∈f c
fill⇒ domc f ∈c c
fill∧ codc f ∈c c
fill∧ (g ∈f c ∧ domc f = codc g
fill⇒ (f of g) ∈f c)
pf_induction
⊢ ∀ p
fill• (∀ f
fill• (∀ g• g ∈f domc f ∨ g ∈f codc f ⇒ p g)
fill⇒ p f)
fill⇒ (∀ f• p f)
Definitions
c
⊢ ∀ c d• c ∈c d ⇔ idf c ∈f d

up quick index

privacy policy

Created:

V