The Theory x003u
Parents
hol
Constants
analytic
's × ('s → 'c → BOOL) → BOOL
sound
(('s → BOOL) × 's → BOOL) × ('s → 'c → BOOL) → 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))
demonstrative
⊢ ∀ sen sem
fill• demonstrative (sen, sem)
fill⇔ (∃ ds• sound (ds, sem) ∧ ds ((λ s• F), sen))
Theorems
Theorem1
⊢ ∀ sen sem
fill• analytic (sen, sem) ⇔ demonstrative (sen, sem)

up quick index

privacy policy

Created:

V