We present two new applications of Simmons'point-free Cantor-Bendixson coderivative operator in intuitionistic logic. First, we use it to give a simplified proof of the recent result of Xu and Ye that the free Heyting algebra on two generators does not occur as the Heyting algebra of subterminal objects in any elementary topos. Then we use it to prove that complete Heyting algebra semantics is not strongly complete for intuitionistic second-order propositional logic: semantic consequence from an arbitrary set of assumptions does not coincide with ordinary syntactic consequence.
We answer the question whether all Heyting algebras can appear as the lattice of subterminal objects of an elementary topos in the negative. Concretely, we show that the free Heyting algebra on two generators, hence also on N generators for every N greater than 2, cannot be such a Heyting algebra. The mathematical resu...
This paper provides an expository comparison of two foundational proof systems in classical propositional logic: Gentzen's sequent calculus and Beth's semantic tableaux. Gentzen's sequent calculus is presented as a rule-based system built upon the single axiom $\alpha \Rightarrow \alpha$, whose key feature — the subfor...
We show that partially ordered sets, lattices, semilattices, Boolean algebras, Heyting algebras with a further coarser or finer partial order, or a linearization, or an auxiliary relation have the strong amalgamation property, Fraïssé limits and, in many cases, an \(\omega\)-categorical model completion with quantifier...
P. Lipparini· Bulletin of the Section of L...· 0 citations
