A note on deduction theorem for Gdel's propositional calculus G4
Ewa Żarnecka-Bial·y, W. A. Pogorzelski's · 2005
In the paper, following W. Pogorzelski's works [4] and [5], I am stating a certain form of deduction theorem valid for G6del's propositional calculus G4 (see [2], p. 4, compare also [6], p. 312)1. Defining below the condition of validity for that theorem I am operating with the concept of a set G, supposing it to be a subset of a set of all the wellformed formulas S, where the set S contains propositional variables p, q, r . . . and is closed under the operation of iuncting the well-formed formulas by the functor of implication -+, coniunction . disjunction + equivalence and also under the operation of prefixing these formulas by the negation functor ~ , as well as by necessity functor L and possibility functor M. The system under consideration I am treating as a substitutionless one, where propositional expressions are denominated by the schematic variables A, B, C, .. . . For a metasystemic implication I am using the sign =~, for metasystemic equivalence the sign ~ ; metasystemic conjunction is expressed by the sign A.