Some examples of different methods of formal proofs with generalizations of the satisfiability definition.
Juliusz Reichbach · Notre Dame Journal of Formal Logic · 1969
This paper 1 is composed of three parts.In the first one we recall my generalization of the usual satisfiability definition, we give a new general variant of my truncated truth definition with it a syntactic picture of sequents; we also construct a generalized diagram introduced here according to the above semantics and [9], and analogous to [5], see also [2], In the second part generalized sequent proof rules based on their semantics of [3] with their generalized diagram are given, and general decidability possibilities for formulas of the first-order functional calculus are supplied; the last method restricts the number of variables to a finite number but possibly with infinite many monadic relations.The third part includes different examples solved by introduced generalized sequent proof rules.The cited papers with our explanations prove the adequacy of the semantic and syntactic considerations.Certain generalizations of the above results will be included in my future papers.We use notions and denotations of [3]-[12] and shortly: alternative +; negation f ; general quantifier Π; free variables x,x u ...\ apparent variables a, ai, . ..; relations signs f\, . . .,/ .=. (M = < D, {ί|} » Λ (φ/(r 1; . . ., n) .=. Fj(s rv ..., s ri ),