Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On semantics of first-order justification logic with binding modalities

Tatiana Yavorskaya, Elena Popova

TL;DR

This paper develops the first-order logic of proofs with binding modalities (FOLP^Box) and provides a Kripke-style semantics using variable valuations via Fitting models. It formalizes axiom systems (FOLP^Box_0 and CS extensions), proves internalization and substitution properties, and then establishes soundness. The core achievement is strong completeness, proven via a canonical Fitting model built from maximal ∃-complete sets and a Truth Lemma that connects syntax to semantics. Overall, the work furnishes a rigorous semantic foundation for first-order justification logics with binding modalities and ties them to canonical modal frameworks.

Abstract

We introduce the first order logic of proofs $FOLP^\Box$ in the joint language combining justification terms and binding modalities. The main issue is Kripke--style semantics for this logic. We describe models for $FOLP^\Box$ in terms of valuations of individual variables instead of introducing constants to the language. This approach requires a new format of the evidence function. This allows us to assign semantic meaning to formulas that contain free variables. The main results are soundness and completeness of $FOLP^\Box$ with respect to the described semantics.

On semantics of first-order justification logic with binding modalities

TL;DR

This paper develops the first-order logic of proofs with binding modalities (FOLP^Box) and provides a Kripke-style semantics using variable valuations via Fitting models. It formalizes axiom systems (FOLP^Box_0 and CS extensions), proves internalization and substitution properties, and then establishes soundness. The core achievement is strong completeness, proven via a canonical Fitting model built from maximal ∃-complete sets and a Truth Lemma that connects syntax to semantics. Overall, the work furnishes a rigorous semantic foundation for first-order justification logics with binding modalities and ties them to canonical modal frameworks.

Abstract

We introduce the first order logic of proofs in the joint language combining justification terms and binding modalities. The main issue is Kripke--style semantics for this logic. We describe models for in terms of valuations of individual variables instead of introducing constants to the language. This approach requires a new format of the evidence function. This allows us to assign semantic meaning to formulas that contain free variables. The main results are soundness and completeness of with respect to the described semantics.

Paper Structure

This paper contains 12 sections, 10 theorems, 27 equations, 3 figures.

Table of Contents

  1. Language and Axioms
  2. Logic $\hbox{\it FOLP}^\Box_{CS}$
  3. Internalization and Substitution in $\hbox{\it FOLP}^\Box_{}$
  4. Semantics
  5. Definition of Fitting Models
  6. Simple Properties and Examples
  7. Soundness
  8. Strong Completeness
  9. Maximal $\exists$--Complete Sets
  10. Canonical Fitting Model
  11. The Truth Lemma
  12. Proof of the Strong Completeness

Key Result

Lemma 1

1. Assume that $p_1,\dots, p_n \in JVar$, $X_1, \dots, X_n$ are finite sets of individual variables and $X = \bigcup\limits_{i=1}^{n} X_i$. If $p_1\! :_{X_1}\!\Phi_1, \dots, p_n\! :_{X_n}\!\Phi_n \vdash_{CS} \Phi,$ then there exist a justification term $t(p_1, \dots,p_n)$ and a constant specificatio 2. If $\Phi_1, \dots, \Phi_n \vdash_{CS} \Phi$ then there is a justification term $t(p_1, \dots p_n

Figures (3)

  • Figure 1: One-point frame with two element domain.
  • Figure 2: Two-point frame with increasing domains.
  • Figure 3: Three-point frame with increasing domains.

Theorems & Definitions (51)

  • Definition 1
  • Remark 1
  • Definition 2
  • Remark 2
  • Definition 3: Constant Specification
  • Example 2
  • Lemma 1: Internalization
  • proof
  • Definition 4
  • Remark 3
  • ...and 41 more