Refine
Document Type
- Working Paper (5) (remove)
Has Fulltext
- yes (5)
Is part of the Bibliography
- no (5)
Keywords
- Logik (5) (remove)
Institute
- Informatik (4)
Es ist wiederholt die These vorgebracht worden, die Grundmuster der europäischen Metaphysik entsprängen den grammatischen Grundmustern der zur Darstellung dieser Metaphysik verwendeten Sprache, allgemeiner des indoeuropäischen Sprachtyps. Was ist z. B. das Sein anderes als eine abstrakte Fiktion, ermöglicht durch die Nominalisierung des Hilfsverbs? Weder findet sich in jeder Sprache ein solches Hilfsverb noch muß überall, wo es vorhanden ist, auch Nominalisierung möglich sein. Ist somit die Rede vom Sein, Ontologie, nicht – unbeschadet der Gründe, um derentwillen diese Rede geübt wird – eine bloße Irreführung durch die Mittel unserer Sprache? Und ferner: Ist nicht die im Wort "Ontologie" erwähnte Logik von eben demselben Sprachbau abhängig (wenn schon nicht von der menschlichen Psyche)? Wir analysieren doch das Urteil in Subjekt, Prädikat und Kopula, S ist P; und auch hier taucht in verräterischer Weise das Hilfsverb auf. Philosophie? Philosophie der Logik? "Die Philosophie ist ein Kampf gegen die Verhexung unseres Verstandes durch die Mittel unserer Sprache." Mit diesen berühmten Worten leitete L. Wittgenstein eine Entwicklung ein ("Wir führen die Wörter von ihrer metaphysischen, wieder auf ihre alltägliche Verwendung zurück.") die E. Tugendhat 1976 schließlich so zusammenfaßte: "Ich kenne keine befriedigende Antwort auf die Frage, wie die sprachanalytische Philosophie von der empirischen Sprachwissenschaft zu unterscheiden ist." Hat das nicht zur Konsequenz, daß am Ende die logisch-philosophischen Probleme – einschließlich aller die Philosophie der Logik betreffenden –, die doch apriori sich aus der Bewußtseinshelle des Menschen herzustellen scheinen, in einer empirischen Disziplin, der Linguistik, aposteriori also, ihre genugtuende Beantwortung finden? Dieser Frage wollen wir nachgehen. Zunächst ist hier kurz zu umreißen, wie sich dem unbefangenen Betrachter die Beziehung von Logik und Linguistik gegenwärtig darstellt.
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. It is designed to perform automatic induction proofs and can also deal with partial functions. This paper provides a reconstruction of the corresponding logic and semantics using the standard treatment of undefinedness which adapts and improves the VeriFun-logic by allowing reasoning on nonterminating expressions and functions. Equality of expressions is defined as contextual equivalence based on observing termination in all closing contexts. The reconstruction shows that several restrictions of the VeriFun framework can easily be removed, by natural generalizations: mutual recursive functions, abstractions in the data values, and formulas with arbitrary quantifier prefix can be formulated. The main results of this paper are: an extended set of deduction rules usable in VeriFun under the adapted semantics is proved to be correct, i.e. they respect the observational equivalence in all extensions of a program. We also show that certain classes of theorems are conservative under extensions, like universally quantified equations. Also other special classes of theorems are analyzed for conservativity.
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. This paper provides a reconstruction of the corresponding logic when partial functions are permitted. Typing is polymorphic for the definition of functions but monomorphic for terms in formulas. Equality of terms is defined as contextual equivalence based on observing termination in all contexts. The reconstruction also allows several generalizations of the functional language like mutual recursive functions and abstractions in the data values. The main results are: Correctness of several program transformations for all extensions of a program, which have a potential usage in a deduction system. We also proved that universally quantified equations are conservative, i.e. if a universally quantified equation is valid w.r.t. a program P, then it remains valid if the program is extended by new functions and/or new data types.
A logical framework consisting of a polymorphic call-by-value functional language and a first-order logic on the values is presented, which is a reconstruction of the logic of the verification system VeriFun. The reconstruction uses contextual semantics to define the logical value of equations. It equates undefinedness and non-termination, which is a standard semantical approach. The main results of this paper are: Meta-theorems about the globality of several classes of theorems in the logic, and proofs of global correctness of transformations and deduction rules. The deduction rules of VeriFun are globally correct if rules depending on termination are appropriately formulated. The reconstruction also gives hints on generalizations of the VeriFun framework: reasoning on nonterminating expressions and functions, mutual recursive functions and abstractions in the data values, and formulas with arbitrary quantifier prefix could be allowed.