| 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  • sound (ds, sem) ⇔ (∀ prem conc • ds (prem, conc) ⇒ (∀ c • (∀ s• prem s ⇒ sem s c) ⇒ sem conc c))
|
|
demonstrative
|
⊢ ∀ sen sem
• demonstrative (sen, sem) ⇔ (∃ ds• sound (ds, sem) ∧ ds ((λ s• F), sen))
|
| Theorems |
|
Theorem1
|
⊢ ∀ sen sem • analytic (sen, sem) ⇔ demonstrative (sen, sem)
|
