Knowing-Value Logic with Successor Arithmetic

In their prior work [7], Wang and Fan proposed conditional knowing-value logic and provided a complete axiomatization.However, in natural language scenarios and logic puzzles, knowing-value reasoning often appears together with arithmetic operations, which motivates us to enrich knowingvalue logic with arithmetic function symbols.In this paper, we extend the language of conditional knowing-value logic with equality and the successor function.Due to the failure of compactness over the class of standard models, we additionally introduce non-standard models to facilitate the technical analysis.Our main results establish the finite model property and provide an axiomatization that is strongly complete with respect to the class of non-standard models and weakly complete with respect to the class of standard models.Furthermore, we extend our logic with public announcement operators and use the resulting system to formalize and solve the "Consecutive Numbers" puzzle.This work provides a novel framework for integrating epistemic logic with arithmetic.Knowing-Value Logic with Successor Arithmetic capture some reasoning in natural language.In natural language, the second statement clearly implies the first.But in ELKv r , K(p → q) does not imply Kv(p, c) because p and q are just independent letters.Generally, reasoning that involves the interaction between equality, knowing-value, and arithmetic is common in natural language scenarios, but ELKv r cannot fully express it.From a semantic perspective, a model for ELKv r assigns values to constants over a bare, unstructured set of objects O.To study specific mathematical structures, such as natural numbers with the successor function (N, 0 N , S N ) or with addition and multiplication (N, 0 N , 1 N , + N , × N ), we must enrich the language with arithmetic function symbols and add arithmetic axioms to the proof system.All these reasons motivate us to enrich knowingvalue logic with equality and arithmetic function symbols, starting with the successor function.To further demonstrate the need for this extension, we present the following puzzle.Example 1.1 ([1]).Anne and Bill get to hear the following: "Given are two natural numbers.They are consecutive numbers.I am going to whisper one of these numbers to Anne and the other number to Bill."This happens.Anne and Bill now have the following conversation.