The Theory x003v
Parents
hol
Constants
analytic
 's × ('s → 'c → BOOL) → BOOL
sound
 (('s → BOOL) × 's → BOOL) × ('s → 'c → BOOL) → BOOL
iiclosed
 (('s → BOOL) × 's → BOOL) → ('s → BOOL) → BOOL
close_ds
 (('s → BOOL) × 's → BOOL) → ('s → BOOL) × 's → BOOL
demonstrative
's × ('s → 'c → BOOL) → BOOL
Definitions
analytic
 ⊢ ∀ sen sem• analytic (sen, sem) ⇔ (∀ c• sem sen c)
sound
 ⊢ ∀ ds sem
fill• sound (ds, sem)
fill⇔ (∀ prem conc
fill• ds (prem, conc)
fill⇒ (∀ c
fill• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c))
iiclosed
 ⊢ ∀ ds ss
fill• iiclosed ds ss
fill⇔ (∀ prems conc
fill• ds (prems, conc) ∧ (∀ s• prems s ⇒ ss s)
fill⇒ ss conc)
close_ds
 ⊢ ∀ ds prems conc
fill• close_ds ds (prems, conc)
fill⇔ (∀ css
fill• iiclosed ds css ∧ (∀ t• prems t ⇒ css t)
fill⇒ css conc)
demonstrative
⊢ ∀ sen sem
fill• demonstrative (sen, sem)
fill⇔ (∃ ds
fill• sound (ds, sem) ∧ close_ds ds ((λ s• F), sen))
Theorems
closure_soundness_lemma
⊢ ∀ ds• sound (ds, sem) ⇔ sound (close_ds ds, sem)
Theorem1
 ⊢ ∀ sen sem
fill• analytic (sen, sem) ⇔ demonstrative (sen, sem)

up quick index

privacy policy

Created:

V