The Theory x003t
Parents
hol
Constants
analytic
's × ('s → BOOL) → BOOL
sound
(('s → BOOL) × 's → BOOL) × ('s → BOOL) → BOOL
demonstrative
's × ('s → BOOL) → BOOL
Definitions
analytic
⊢ ∀ sen sem• analytic (sen, sem) ⇔ sem sen
sound
⊢ ∀ ds sem
fill• sound (ds, sem)
fill⇔ (∀ prem conc
fill• ds (prem, conc)
fill⇒ (∀ s• prem s ⇒ sem s)
fill⇒ sem conc)
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