On Infinitary G\"odel logics

TL;DR

This paper develops and proves completeness theorems for infinitary G"odel logics, extending classical propositional and first-order logics to countably infinite conjunctions and disjunctions with algebraic and proof-theoretic methods.

Contribution

It introduces infinitary Hilbert-style and hypersequent calculi for G"odel logics and establishes their completeness and cut-elimination properties.

Findings

Completeness theorems for infinitary propositional and first-order G"odel logics.

Development of infinitary Hilbert-style calculi with countable conjunctions and disjunctions.

Cut-elimination results for infinitary hypersequent calculi.

Abstract

We study propositional and first-order G\"odel logics over infinitary languages which are motivated semantically by corresponding interpretations into the unit interval [0,1]. We provide infinitary Hilbert-style calculi for the particular (propositional and first-order) cases with con-/disjunctions of countable length and prove corresponding completeness theorems by extending the usual Lindenbaum-Tarski construction to the infinitary case for a respective algebraic semantics via complete linear Heyting algebras. We provide infinitary hypersequent calculi and prove corresponding cut-elimination theorems in the Sch\"utte-Tait-style. Initial observations are made regarding truth-value sets other than [0,1].