|
On the second order intuitionistic propositional logic without a universal quantifier| old_uid | 5612 |
|---|
| title | On the second order intuitionistic propositional logic without a universal quantifier |
|---|
| start_date | 2008/11/17 |
|---|
| schedule | 14h-16h |
|---|
| online | no |
|---|
| summary | We examine second order intuitionistic propositional logic, IPC2. Let F9 be the set of formulas with no universal quantification. We prove Glivenko’s theorem for formulas in F9 that is, for ' 2 F9, ' is a classical tautology if and only if ¬¬' is a tautology of IPC2. We show that for each sentence ' 2 F9 (without free variables), ' is a classical tautology if and only if ' is an intuitionistic tautology. As a corollary we obtain a semantic argument that the quantifier 8 is not
definable in IPC2 from ?,_,^,!, 9. |
|---|
| responsibles | Bonnay, Sandu |
|---|
| |
|