Occurrences and Substitutions
While usually the syntactic entities (as terms, formulae and formula trees) are treated carefully in logic and related elds, this is not true anymore with respect to the treatment of their occurrences. A brief survey of the literature yields a great variety of intuitive and/or inaccurate approaches; the best denition is found in computer science (for example, Huet [2]), but the proposed theory of occurrences is too weak to represent this concept in its full strength.
While usually the syntactic entities (as terms, formulae and formula trees) are treated carefully in logic and related elds, this is not true anymore with respect to the treatment of their occurrences. A brief survey of the literature yields a great variety of intuitive and/or inaccurate approaches; the best denition is found in computer science (for example, Huet [2]), but the proposed theory of occurrences is too weak to represent this concept in its full strength.
This unsatisfactory situation was the motivation to investigate in our dissertation [1] the notion of occurrences in some detail. Thereby, an occurrence is determined by three aspects: an occurrences is always an occurrence of a syntactic entity (its shape) in a syntactic entity (its context) at a specic position. Context and shape are meaningful combinations of the well-known syntactic entities. Our crucial idea is to represent the positions by the so called nominal forms as introduced by Schütte [4]; as a consequence, we obtain a strong and general theory of occurrences.
This unsatisfactory situation was the motivation to investigate in our dissertation [1] the notion of occurrences in some detail. Thereby, an occurrence is determined by three aspects: an occurrences is always an occurrence of a syntactic entity (its shape) in a syntactic entity (its context) at a specic position. Context and shape are meaningful combinations of the well-known syntactic entities. Our crucial idea is to represent the positions by the so called nominal forms as introduced by Schütte [4]; as a consequence, we obtain a strong and general theory of occurrences.
1. In the first session of the tutorial, we introduce the formal notion of occurrences together with central methods needed for their treatment. We illustrate the capacity of this theory to address typical problems concerning occurrences, which are not solvable only on the base of the inductive denitions of the underlying syntactic entities, but require a good representation of the position. If time permits, the introduction is complemented by a brief survey of the traditional approaches to occurrences.
1. In the first session of the tutorial, we introduce the formal notion of occurrences together with central methods needed for their treatment. We illustrate the capacity of this theory to address typical problems concerning occurrences, which are not solvable only on the base of the inductive denitions of the underlying syntactic entities, but require a good representation of the position. If time permits, the introduction is complemented by a brief survey of the traditional approaches to occurrences.
2. In the second session, we discuss the so called formal substitutions, which are a canonical generalisation of occurrences. These substitutions represent the process of replacing in a syntactic entity some occurrences by suitable arguments. The use of this concept is illustrated by representing informal mathematical calculations with the help of such substitutions. The relationship between substitutions and substitution functions (understood as usual) is considered.
2. In the second session, we discuss the so called formal substitutions, which are a canonical generalisation of occurrences. These substitutions represent the process of replacing in a syntactic entity some occurrences by suitable arguments. The use of this concept is illustrated by representing informal mathematical calculations with the help of such substitutions. The relationship between substitutions and substitution functions (understood as usual) is considered.
3. The last session is devoted to a central notion of logic: derivations in Natural Deduction. Due to the discharge function, the notion of a derivation depends strongly on the concept of occurrences. We provide an adequate and detailed definition of derivations in the light of a suitable theory of occurrences (surprisingly and in contrast to Prawitz's suggestion [3] without recourse to formula occurrences). Conceptual choices will be uncovered and the impact of different requirements concerning derivations will be discussed.
3. The last session is devoted to a central notion of logic: derivations in Natural Deduction. Due to the discharge function, the notion of a derivation depends strongly on the concept of occurrences. We provide an adequate and detailed definition of derivations in the light of a suitable theory of occurrences (surprisingly and in contrast to Prawitz's suggestion [3] without recourse to formula occurrences). Conceptual choices will be uncovered and the impact of different requirements concerning derivations will be discussed.
References
References
[1] Rene Gazzari, Formal Theories of Occurrences and Substitutions, Ph.D. thesis, University of Tübingen, 2020.
[1] Rene Gazzari, Formal Theories of Occurrences and Substitutions, Ph.D. thesis, University of Tübingen, 2020.
[2] Gerard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal of the Association for Computing Machinery 27 (1980), no. 4, 797{821.
[2] Gerard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal of the Association for Computing Machinery 27 (1980), no. 4, 797{821.
[3] Dag Prawitz, Natural Deduction: A Proof-Theoretical Study, Almqvist & Wiksell, Stockholm, 1965.
[3] Dag Prawitz, Natural Deduction: A Proof-Theoretical Study, Almqvist & Wiksell, Stockholm, 1965.
[4] Kurt Schütte, Proof Theory, Grundlehren der mathematischen Wissenschaften, vol. 225, Springer-Verlag Berlin Heidelberg, 1977.
[4] Kurt Schütte, Proof Theory, Grundlehren der mathematischen Wissenschaften, vol. 225, Springer-Verlag Berlin Heidelberg, 1977.