Die Mathe-Redaktion - 17.08.2019 20:21 - Registrieren/Login
Auswahl
ListenpunktHome
ListenpunktAktuell und Interessant ai
ListenpunktArtikelübersicht/-suche
ListenpunktAlle Links / Mathe-Links
ListenpunktFach- & Sachbücher
ListenpunktMitglieder / Karte / Top 15
ListenpunktRegistrieren/Login
ListenpunktArbeitsgruppen
Listenpunkt? im neuen Schwätz
ListenpunktWerde Mathe-Millionär!
ListenpunktAnmeldung MPCT Sept.
ListenpunktFormeleditor fedgeo
Schwarzes Brett
Aktion im Forum
Suche
Stichwortsuche in Artikeln und Links von Matheplanet
Suchen im Forum
Suchtipps

Bücher
Englische Bücher
Software
Suchbegriffe:
Mathematik bei amazon
Naturwissenschaft & Technik
In Partnerschaft mit Amazon.de
Kontakt
Mail an Matroid
[Keine Übungsaufgaben!]
Impressum

Bitte beachten Sie unsere Nutzungsbedingungen, die Distanzierung, unsere Datenschutzerklärung und
die Forumregeln.

Sie können Mitglied werden. Mitglieder können den Matheplanet-Newsletter bestellen, der etwa alle 2 Monate erscheint.

Der Newsletter Okt. 2017

Für Mitglieder
Mathematisch für Anfänger
Wer ist Online
Aktuell sind 352 Gäste und 15 Mitglieder online.

Sie können Mitglied werden:
Klick hier.

Über Matheplanet
 
Zum letzten Themenfilter: Themenfilter:
Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Logik, Mengen & Beweistechnik » Prädikatenlogik » Formalisierung des Modellbegriffs?
Druckversion
Druckversion
Antworten
Antworten
Autor
Universität/Hochschule Formalisierung des Modellbegriffs?
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Themenstart: 2019-07-02


Hallo allerseits,
I)
Eine mathematische Theorie wird (meistens) in der Prädikatenlogik 1. Stufe (PL1) formuliert, wie z.B. das Peanosche Axiomensstem (PA).

Man hat also:
1) die Sprache L, also eine Menge von Formeln, die man syntaktisch definiert.
2) Eine Interpretation I, die aus einer Struktur und einer Belegungsfunktion h besteht.
Dadurch bekommt eine Formel eine Bedeutung.

II)
Die Sprache L ist also voll formalisiert. Was ist aber mit der Interpretation einer Formel.
Wie wird diese formalisiert?

Beispiel: (siehe Definition bei Ebbinghaus):
Es sei A eine Trägermenge und h eine Belegung und $\mathfrak{I}=(A,h)$
Dann wird definiert:
$\mathfrak{I} \models \forall x \varphi$ gdw: für alle a $\in$ A gilt: $\mathfrak{I}_{x}^{a} \models \varphi$
Im rechten Teil von gdw kommt also der _informale_ Begriff für alle vor.

III)
Frage:
Wie wird ein Modell also voll formalisiert ?

Beispiel:
Bei PA gibt es das sogenannte Standardmodell.
Darin könnte man z.B. formulieren:
Für alle x,y gilt: x+y=y+x
Wie wird das formalisert?
Den Allquantor kann man nicht verwenden, denn dieser ist nur in PL1 definiert, aber nicht in der Interpretation.

mfg
cx









  Profil  Quote  Link auf diesen Beitrag Link
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 1574
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.1, eingetragen 2019-07-03

\(\begingroup\)\( \newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\)
2019-07-02 15:35 - carlox im Themenstart schreibt:
Hallo allerseits,
I)
Eine mathematische Theorie wird (meistens) in der Prädikatenlogik 1. Stufe (PL1) formuliert, wie z.B. das Peanosche Axiomensstem (PA).

Man hat also:
1) die Sprache L, also eine Menge von Formeln, die man syntaktisch definiert.
2) Eine Interpretation I, die aus einer Struktur und einer Belegungsfunktion h besteht.
Dadurch bekommt eine Formel eine Bedeutung.
"Man hat" nicht "eine Interpretation". Man spricht später über *viele* Interpretationen und Belegungen.

II)
Die Sprache L ist also voll formalisiert. Was ist aber mit der Interpretation einer Formel.
Wie wird diese formalisiert?

Eine Interpretation kommt üblicherweise mit einer Trägermenge und mit Interpretationen für die Funktions- und Relationssymbole.
Die Bedeutung einer Formel bzgl einer Belegung wird rekursiv über den Formel- und Termaufbau definiert.

Beispiel: (siehe Definition bei Ebbinghaus):
Es sei A eine Trägermenge und h eine Belegung und $\mathfrak{I}=(A,h)$
Dann wird definiert:
$\mathfrak{I} \models \forall x \varphi$ gdw: für alle a $\in$ A gilt: $\mathfrak{I}_{x}^{a} \models \varphi$
Im rechten Teil von gdw kommt also der _informale_ Begriff für alle vor.
"informal" ist hier nur irreführend. Es wird einfach die Sprache benutzt, in der man auch definiert hat, wie Formeln aussehen dürfen, was eine Interpretation ist, etc. (die "Metasprache") Die kann so formal oder informal sein, wie es sich eben ergibt.

III)
Frage:
Wie wird ein Modell also voll formalisiert ?

Beispiel:
Bei PA gibt es das sogenannte Standardmodell.
Darin könnte man z.B. formulieren:
Für alle x,y gilt: x+y=y+x
Wie wird das formalisert?
Den Allquantor kann man nicht verwenden, denn dieser ist nur in PL1 definiert, aber nicht in der Interpretation.

mfg
cx
Man kann natürlich auch in der Metasprache Quantoren haben.

Hier mal ein wenig Lean-Code. Hier ist die Metasprache eben Lean, FOL-Formeln können zwar Quantoren enthalten, die aber nicht mit dem Glyph ∀ geschrieben werden, und in der Semantik von Formeln wird u.a. das Lean-∀ benutzt, um zu sagen, was Objekt-Sprachen-Formeln mit Allquantor bedeuten.
Lean
section AnFOL
 
parameter {F: Type}
parameter {R: Type}
 
-- For simplicity, we take arbitrary types instead of 
-- natural numbers or cardinals as arities.
parameter ar_F: F  Type
parameter ar_R: R  Type
 
-- terms, parameterized by a type of allowed free variables
inductive Term(V: Type)
    | var{}: V  Term
    | app{}: Π f: F, (ar_F f  Term)  Term    
 
-- formulas, with "locally nameless" encoding of variables
inductive Form: Type  Type.{1}
    | eql{}:   Π {V: Type}, Term V  Term V  Form V
    | rel:     Π {V: Type} (r: R), (ar_R r  Term V)  Form V
    | all:     Π {V: Type}, Form (option V)  Form V
    | ex:      Π {V: Type}, Form (option V)  Form V
    | and:     Π {V: Type}, Form V  Form V  Form V
    | or:      Π {V: Type}, Form V  Form V  Form V
    | impl:    Π {V: Type}, Form V  Form V  Form V
    | not:     Π {V: Type}, Form V  Form V
    | true{}:  Π {V: Type}, Form V
    | false{}: Π {V: Type}, Form V
 
-- what's a structure?
structure Structure := mk ::
    (carrier: Type)
    (intpF: Π f: F, (ar_F f  carrier)  carrier)
    (intpR: Π r: R, (ar_R r  carrier)  Prop)
 
-- semantics of terms under assignments
def intpT(S: Structure){V: Type}: Term V  (V  S.carrier)  S.carrier
    | (Term.var v) b := b v
    | (Term.app f x) b := S.intpF f $ λ i, intpT (x i) b
 
def focus{V: Type}{X: Type}(x: X)(b: V  X): option V  X := λ w,
    match w with
        | none := x
        | some v := b v
    end
 
-- semantic of formulas under assignments
def intpF(S: Structure): Π {V: Type}, Form V  (V  S.carrier)  Prop
    | V (Form.eql  t u) b := intpT S t b = intpT S u b
    | V (Form.rel  r x) b := S.intpR r $ λ i, intpT S (x i) b
    | V (Form.all  φ)   b :=  x: S.carrier, intpF φ $ focus x b
    | V (Form.ex   φ)   b :=  x: S.carrier, intpF φ $ focus x b
    | V (Form.and  φ ψ) b := intpF φ b  intpF ψ b
    | V (Form.or   φ ψ) b := intpF φ b  intpF ψ b
    | V (Form.impl φ ψ) b := intpF φ b  intpF ψ b
    | V (Form.not  φ)   b := ¬ intpF φ b
    | V (Form.false)    b := false
    | V (Form.true)     b := true
 
parameter {AxI: Type*}
-- We take only closed formulas as axioms. For FOL that's sufficient.
parameter Axioms: AxI  Form empty
 
def isModel(S: Structure): Prop :=  i: AxI, intpF S (Axioms i) $ λ x: empty, x.cases_on _
 
-- some syntactical operations
def gsubstT{V: Type}: Term V  Π {W: Type}, (V  Term W)  Term W
    | (Term.var v)   W h := h v
    | (Term.app f x) W h := Term.app f $ λ i, gsubstT (x i) h
 
def mapT{V W: Type}(f: V  W): Term V  Term W := λ t, gsubstT t (Term.var ∘ f)
 
def alift{V W: Type}(h: V  Term W): option V  Term (option W) := λ v,
    match v with
        | none := Term.var none
        | some v := mapT option.some $ h v
    end
 
def gsubstF: Π {V: Type}, Form V  Π {W: Type}, (V  Term W)  Form W
    | V (Form.eql  t u) W h := Form.eql (gsubstT t h) (gsubstT u h)
    | V (Form.rel  r x) W h := Form.rel r $ λ i, gsubstT (x i) h
    | V (Form.all  φ)   W h := Form.all $ gsubstF φ $ alift h
    | V (Form.ex   φ)   W h := Form.ex  $ gsubstF φ $ alift h
    | V (Form.and  φ ψ) W h := Form.and  (gsubstF φ h) (gsubstF ψ h)
    | V (Form.or   φ ψ) W h := Form.or   (gsubstF φ h) (gsubstF ψ h)
    | V (Form.impl φ ψ) W h := Form.impl (gsubstF φ h) (gsubstF ψ h)
    | V (Form.not  φ)   W h := Form.not  (gsubstF φ h)
    | V (Form.false)    W h := Form.false
    | V (Form.true)     W h := Form.true
 
end AnFOL
 
section Peano
 
inductive F 
    | zero 
    | succ 
    | plus 
    | mult
 
def peano_arF(f: F): Type := match f with
    | F.zero := empty
    | F.succ := unit
    | F.plus := bool
    | F.mult := bool
end
 
def peano_arR(x: empty): Type := x.cases_on _
 
-- not pretty, but it works
def peanoAxiomsI := option $ option $ option $ option $ Form peano_arF peano_arR (option empty)
def peanoAxioms(i: peanoAxiomsI): Form peano_arF peano_arR empty := match i with
    -- zero not in the image of succ
    | none := Form.all $ Form.not $ Form.eql 
        (Term.app F.zero (λ i, i.cases_on _)) 
        (Term.app F.succ (λ _, Term.var none))
    -- succ injective
    | some none := Form.all $ Form.all $
        Form.impl 
            (Form.eql (Term.app F.succ $ λ _, Term.var none) (Term.app F.succ $ λ _, Term.var $ some $ none)) 
            (Form.eql (Term.var none) (Term.var $ some none))
    | some (some none) := sorry             -- axiomatisation of +, * omitted
    | some (some (some none)) := sorry
    -- induction scheme, only for formulas with *at most* one free variable;
    -- should only be awkward to use, not insufficient.
    | some (some (some (some φ))) := 
        Form.impl (Form.and (gsubstF peano_arF peano_arR φ $ λ _, Term.app F.zero $ λ x, x.cases_on _) $ 
            Form.all $ Form.impl φ (gsubstF peano_arF peano_arR φ (λ v, match v with 
                | none := Term.app F.succ $ λ _, Term.var none
                | els := Term.var els
            end))) (Form.all φ)
end
 
def StdModel: Structure peano_arF peano_arR := {
    carrier := ,
    intpF := λ f, match f with
        | F.zero := λ xs, 0
        | F.succ := λ xs, nat.succ $ xs ()
        | F.plus := λ xs, xs ff + xs tt
        | F.mult := λ xs, xs ff * xs tt
    end,
    intpR := λ r, match r with end
}
 
theorem is_model: isModel peano_arF peano_arR peanoAxioms StdModel := sorry
 
end Peano

\(\endgroup\)


  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.2, vom Themenstarter, eingetragen 2019-07-03


Hallo tactac
Erst Mal vielen, herzlichen Dank für deine email und vor allem auf den wertvollen Hinweis auf die Programmiersprache Lean.
Das ist sehr viel Infomaterial, das ich natürlich noch nicht verarbeitet habe.

1)
Ich habe nur mal was von der Programmiersprache Coq gehört (siehe Wikipedia).
Was ist der Unterschied zwischen Lean und Coq (was kann mehr?)
Vor allem:  was ist einfacher zu erlernen (man sollte erst mal mit Einfacherem beginnen).

2)
Habe mal kurz in Lean reingeschaut.
Dort gibt es die uns bekannte Quantorzeichen  $\forall$ und   $\exists$
>
>Hier mal ein wenig Lean-Code. Hier ist die Metasprache eben Lean,
>FOL-Formeln können zwar Quantoren enthalten, die aber nicht
>mit dem Glyph ∀ geschrieben werden, und in der Semantik von
>Formeln wird u.a. das Lean-∀ benutzt, um zu sagen,
>was Objekt-Sprachen-Formeln mit Allquantor bedeuten.
>
Ich habe mich nur flüchtig mit Lean beschäftigt, aber:
a) Warum kann man in FOL-Formeln einen Allquantor nicht mit dem Glyph ∀ schreiben (wie macht man das sonst)?
b) Kann man in  Lean sowohl die Objektsprache (z.B. mit FOL) UND die Metasprache gleichzeitig verwenden ?      
c) Kennst du auch  eine deutsche Doku zu Lean ?

3)
>
>"informal" ist hier nur irreführend. Es wird einfach die Sprache benutzt,
>in der man auch definiert hat, wie Formeln aussehen dürfen, was eine
>Interpretation ist, etc. (die "Metasprache")
>Die kann so formal oder informal sein, wie es sich eben ergibt.
>
Konkret zur Metasprache:
Meine Vorstellung:
Beim Standardmodell von PA verwendet man doch die Schulmathematik:
Addition, Multiplikation und die "naiven" Zahlen (Kindergartenzahlen) 0,1,2,3…
Das muss dann alles in Lean enthalten sein, also auch der Algorithmus  der Addition (dieser benutzt vermutlich den ADD-Assemblerbefehl).
Ist meine Vorstellung korrekt ?

Mfg
cx



  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 190
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.3, eingetragen 2019-07-03


Man muß bei dieser Fragestellung erst gar nicht die Peano Arithmetik bemühen, das Problem tritt schon bei der Aussagenlogik auf. Hier wird die Semantik der aussagenlogischen Verknüpfungen üblicherweise durch Wahrheitstafeln definiert. Aber Wahrheitstafeln sind metasprachliche Objekte bei denen unterstellt wird, daß deren Bedeutung "schon klar" ist. Natürlich kann man die Semantik von Wahrheitstafeln auch mathematisch formal definieren. Nur ist dazu wieder eine Metasprache erforderlich, deren Semantik "geglaubt" wird. Auch diese Metasprache kann mathematisch formal definiert werden, nur braucht man dazu wieder eine Metasprache.

In einem Beweisassistenten (wie etwa COQ oder ISABELLE) kann man sowohl einen korrekten und vollständigen Kalkül für die Prädikatenlogik 1. Stufe mathematisch formal definieren als auch die Semantik der prädikatenlogischen Sprache, und dann formal Korrektheit und Vollständigkeit des Kalküls beweisen. Insoweit fehlt hier scheinbar die Metasprache. Aber der Beweisassistent ist in einer Programmiersprache programmiert, deren Semantik die Semantik der Ergebnisse des Programms festlegt. Natürlich kann man die Semantik der Programmiersprache formal definieren, aber dazu benötigt man wieder eine Metasprache ... (s.o).

Man könnte jetzt einwenden, wenn schon gewisse Annahmen geglaubt werden müssen, so kann man doch die ganze Beweiserei lassen und eben alles, was einem plausibel erscheint (etwa die Gültigkeit des Fermatschen Satzes) einfach glauben. Eine implizite Forderung an metasprachliche Definitionen ist jedoch, daß diese einfach und allgemein als verständlich anerkannt sind. Es wird sich wohl niemand finden, der über die Bedeutung des metasprachlichen Begriffs "für alle" im Zweifel ist (vorausgesetzt man versteht Deutsch). Dagegen ist der Glaube an die Gültigkeit des Fermatschen Satzes (anstatt des Beweises) eine Zumutung.    

PS: Metasprache ist nicht nur für die Definition der Semantik erfordlich, sondern auch für die Syntax. Beispiel: "Sind A und B prädikatenlogische Formeln, so ist auch A v B eine prädikatenlogische Formel."



  Profil  Quote  Link auf diesen Beitrag Link
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 1574
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.4, eingetragen 2019-07-06

\(\begingroup\)\( \newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\)
2019-07-03 15:08 - carlox in Beitrag No. 2 schreibt:
1)
Ich habe nur mal was von der Programmiersprache Coq gehört (siehe Wikipedia).
Was ist der Unterschied zwischen Lean und Coq (was kann mehr?)
Vor allem:  was ist einfacher zu erlernen (man sollte erst mal mit Einfacherem beginnen).
Die Logik von beiden basiert auf dem "Calculus of inductive constructions". Beide bieten Typklassen. Unterschiede gibt es hauptsächlich in der oberflächlichen Syntax, und den Möglichkeiten, Notationen und eigene Taktiken zu definieren.
Es ist nicht so, dass "Lean" oder "Coq" die korrekte Antwort auf die Frage "was kann mehr?" wäre, würde ich sagen. Es ist auch nicht so, dass eins von beiden einfacher zu erlernen wäre. Mir kommen sie in der Hinsicht ziemlich ähnlich vor.

2)
Habe mal kurz in Lean reingeschaut.
Dort gibt es die uns bekannte Quantorzeichen  $\forall$ und   $\exists$
>
>Hier mal ein wenig Lean-Code. Hier ist die Metasprache eben Lean,
>FOL-Formeln können zwar Quantoren enthalten, die aber nicht
>mit dem Glyph ∀ geschrieben werden, und in der Semantik von
>Formeln wird u.a. das Lean-∀ benutzt, um zu sagen,
>was Objekt-Sprachen-Formeln mit Allquantor bedeuten.
>
Ich habe mich nur flüchtig mit Lean beschäftigt, aber:
a) Warum kann man in FOL-Formeln einen Allquantor nicht mit dem Glyph ∀ schreiben (wie macht man das sonst)?
Das FOL, von dem ich sprach, war die Objektsprache, um die es in meinem Code ging. Der induktive Typ Form gibt da an, wie FOL-Formeln aussehen dürfen, und legt für allquantisierte Formeln den Konstruktor Form.all fest. $\forall$ dagegen steht normalerweise für das "Lean-$\forall$". Ob es eine Möglichkeit gibt, $\forall$ je nach Kontext auch mal für Form.all stehen zu lassen, weiß ich nicht 100%ig. Bin mir ziemlich sicher, dass es in Lean 3 nicht geht. In Lean 4 vielleicht.

b) Kann man in  Lean sowohl die Objektsprache (z.B. mit FOL) UND die Metasprache gleichzeitig verwenden ?
Was soll "die Objektsprache" sein?

c) Kennst du auch  eine deutsche Doku zu Lean ?
Nein.

3)
>
>"informal" ist hier nur irreführend. Es wird einfach die Sprache benutzt,
>in der man auch definiert hat, wie Formeln aussehen dürfen, was eine
>Interpretation ist, etc. (die "Metasprache")
>Die kann so formal oder informal sein, wie es sich eben ergibt.
>
Konkret zur Metasprache:
Meine Vorstellung:
Beim Standardmodell von PA verwendet man doch die Schulmathematik:
Addition, Multiplikation und die "naiven" Zahlen (Kindergartenzahlen) 0,1,2,3…
Das muss dann alles in Lean enthalten sein, also auch der Algorithmus  der Addition (dieser benutzt vermutlich den ADD-Assemblerbefehl).
Ist meine Vorstellung korrekt ?
"Das Standardmodell" für PA gibt es eigentlich nicht. Wenn man eins angeben will oder muss, verwendet man üblicherweise das aus der Metasprache. Üblicherweise ist soetwas auch tatsächlich und beinahe zwingend vorhanden, denn wenn man sagen kann, was Formeln sind, dann auf völlig analoge Weise (mit anderen Konstruktoren) auch, was natürliche Zahlen sind. In Lean zum Beispiel ist etwas wie folgendes vordefiniert:
Lean
inductive Nat 
    | zero: Nat 
    | succ: Nat  Nat
Dies stellt ein Induktionsprinzip zur Verfügung und die Möglichkeit, Funktionen rekursiv zu definieren etc.
Es wird aber eigentlich abstrakt geblieben. Mit einem Assembler-Befehl ADD hat das nichts zu tun.
\(\endgroup\)


  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.5, vom Themenstarter, eingetragen 2019-07-06


Hallo Zwerg_Allwissend,
1)
(2019-07-03 17:21 - Zwerg_Allwissend in <a
Aber der Beweisassistent ist in einer Programmiersprache programmiert, deren Semantik die Semantik der Ergebnisse des Programms festlegt.
Das habe ich leider nicht verstanden. Kannst du mir das bitte genauer (vielleicht an einem Beispiel) erklären ?

2)

href=viewtopic.php?topic=242584&post_id=1766331>Beitrag No. 3)
PS: Metasprache ist nicht nur für die Definition der Semantik erfordlich, sondern auch für die Syntax. Beispiel: "Sind A und B prädikatenlogische Formeln, so ist auch A v B eine prädikatenlogische Formel."
Du meinst die Definition von Termen und Formel in der Metasprache.
Terme und Formeln werden mit induktiv definierten Mengen (deren Grundlage die Mengenlehre ist) formalisiert. Dahinter steckt der Kleensche Fixpunktsatz.
Induktiv definierten Mengen (und die Mengenlehre) sind aber alles andere als " einfach und allgemein verständlich".
Was meinst du dazu ?

3)

"Sind A und B prädikatenlogische Formeln, so ist auch A v B eine prädikatenlogische Formel."
Das fängt schon viel früher an:
Bei der Definition der Syntax, muss man irgendwann ja die Bezeichnung Variablen, Relationssymbole und Funktionssymbole erwähnen. Diese Erwähnung muss man in einer Sprache formulieren. Das muss ja eine natürliche Sprache wie z.B. Englisch oder Deutsch sein.

4) Beweisbarkeit in der Metasprache formulieren.
Bei einem "normalen" mathemtischem Beweis (also nicht der formale Ableitungsbegriff in der Prädikatenlogik) werden stillschweigend Annahmen (Schlussregeln, usw.) getroffen und benutzt, die die nirgends in der Metasprache spezifiziert werden (ist eigentlich intellektuell unredlich).
Ein in der Metasprache angegebener Beweis ist m.M. nach ähnlich einem Beweis in FOL. Nur ist ein FOL-Beweis formal spezifiziert.

5)
Weiss jemand einen Link (oder Literatur), der sich mit dieser Problematik auseinandersetzt?


mfg
cx










  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 190
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.6, eingetragen 2019-07-08


2019-07-06 08:07 - carlox in Beitrag No. 5 schreibt:
Hallo Zwerg_Allwissend,
1)
(2019-07-03 17:21 - Zwerg_Allwissend in <a
Aber der Beweisassistent ist in einer Programmiersprache programmiert, deren Semantik die Semantik der Ergebnisse des Programms festlegt.
Das habe ich leider nicht verstanden. Kannst du mir das bitte genauer (vielleicht an einem Beispiel) erklären ?

2)

href=viewtopic.php?topic=242584&post_id=1766331>Beitrag No. 3)
PS: Metasprache ist nicht nur für die Definition der Semantik erfordlich, sondern auch für die Syntax. Beispiel: "Sind A und B prädikatenlogische Formeln, so ist auch A v B eine prädikatenlogische Formel."
Du meinst die Definition von Termen und Formel in der Metasprache.
Terme und Formeln werden mit induktiv definierten Mengen (deren Grundlage die Mengenlehre ist) formalisiert. Dahinter steckt der Kleensche Fixpunktsatz.
Induktiv definierten Mengen (und die Mengenlehre) sind aber alles andere als " einfach und allgemein verständlich".
Was meinst du dazu ?

3)

"Sind A und B prädikatenlogische Formeln, so ist auch A v B eine prädikatenlogische Formel."
Das fängt schon viel früher an:
Bei der Definition der Syntax, muss man irgendwann ja die Bezeichnung Variablen, Relationssymbole und Funktionssymbole erwähnen. Diese Erwähnung muss man in einer Sprache formulieren. Das muss ja eine natürliche Sprache wie z.B. Englisch oder Deutsch sein.

4) Beweisbarkeit in der Metasprache formulieren.
Bei einem "normalen" mathemtischem Beweis (also nicht der formale Ableitungsbegriff in der Prädikatenlogik) werden stillschweigend Annahmen (Schlussregeln, usw.) getroffen und benutzt, die die nirgends in der Metasprache spezifiziert werden (ist eigentlich intellektuell unredlich).
Ein in der Metasprache angegebener Beweis ist m.M. nach ähnlich einem Beweis in FOL. Nur ist ein FOL-Beweis formal spezifiziert.

5)
Weiss jemand einen Link (oder Literatur), der sich mit dieser Problematik auseinandersetzt?

Ich versuche noch mal eine Anwort:

Bleiben wir bei dem Beispiel Prädikatenlogik 1. Stufe (FOL). In Lehrbüchern wie von Ebbinghaus wird die prädikatenlogische Sprache, also die Objektsprache, definiert sowie deren Semantik (Modellbegriff, Allgemeingültigkeit etc.). Diese Definitionen werden in natürlicher Sprache formuliert - das ist hier die Metasprache.

Deine Ausgangsfrage hat zweierlei Aspekte:

(A) Kann man die natürliche Sprache als Metasprache loswerden?

(B) Falls ja, wie wird man sie los?

Die Antwort zu (A) lautet sowohl "ja" als auch "nein". "Ja" insoweit, da man die Definition der prädikatenlogischen Sprache sowie deren Semantik mittels eines mathematischen Formalismus definieren kann ohne natürliche Sprache zu verwenden. 'tactac' hat das ja in #1 mittels des Formalismus von Lean demonstriert, Metasprache ist hier also die Lean-Sprache. Um jedoch zu verstehen, was er da genau gemacht hat, muß man die Semantik der Lean-Sprache kennen. Möglicherweise wird diese durch einen anderen Formalismus mathematisch präzise definiert, etwa mittels des λ-Kalküls - der ist dann Metasprache (bzgl. der Lean-Sprache als Objektsprache). Um das nun wieder zu verstehen müssen wir Sprache und Semantik des λ-Kalküls kennen. Man kann das jetzt immer so weiter treiben, nur am Ende muß man immer auf natürliche Sprache als Metasprache zurückgreifen. D.h., die natürliche Sprache wird man nie los, daher das "nein".

(B) Das hat 'tactac' in #1 für das Beispiel mittels Lean gezeigt. Ein allgemeines Rezept wie man aus natürlich-sprachlichen Definitionen formale Definitionen gewinnt gibt es nicht. Klar ist nur, daß man hier Logik höherer Stufe benötigt, da man über Funktionen quantifizieren muß. Ich denke, daß das auch generell so sein muß, d.h. die formale Metasprache muß immer ausdrucksstärker als die formale Objektsprache sein.

Zu Deine weiteren Fragen:

1) Wenn Du ein Programm in einer Programmiersprache schreibst, so hängen die Ergebnisse Deines Programms nicht nur davon ab, was Du programmiert hast, sondern auch von der Semantik der Programmiersprache. D.h., wenn bei Implementierung der Programmiersprache + mit * verwechselt wurde wirst Du Dich über das Ergebnisse Deines Programms wundern. Denn immer wenn Du in Deinem Programm addierst, wird bei Ausführung des Programms multipliziert.

2) Ohne den Ebbinghaus jetzt zur Hand zu haben gehe ich fest davon aus, daß Terme und Formeln dort natürlich-sprachlich definiert werden (und bestimmt nicht mittels des Kleenschen Fixpunktsatzes, den man dafür überhaupt nicht braucht).

3) Tatsächlich findet man in mathematischen Aufsätzen um die 30er Jahre des letzten Jahrhunderts Kapitel, in denen zunächst bewiesen wird, daß man von der Existenz abzählbarer Mengen von Variablensymbolen, Funktionssymbolen usw. tatsächlich ausgehen darf. Aber die Definition solcher Mengen muß nicht notwendigerweise in natürlicher Sprache erfolgen - s. die Lean-Formalisierung aus #1.

4) Formale Logik ist aus der Grundlagenkrise der Mathematik zu Beginn des letzten Jahrhunderts entstanden. Das Problem war, wie aussagekräftig Ergebnisse der Mathematik sind, wenn deren Nachweis lediglich informell, also nicht-mathematisch ist. Ergebnis war die Formalisierung des mathematischen Schließens sowie Beweise über die Mächtigkeit verschiedener Kalküle und Theorien (entscheidbar, semi-entscheidbar, nicht semi-entscheidbar). Die Formale Logik wurde als Werkzeug entwickelt, um Aussagen ÜBER das mathematische Schließen zu treffen, und nicht als Werkzeug um mathematische Beweise ZU FÜHREN. Letzteres ist erst mit der Entwicklung von Computern interessant geworden, denn formale Beweise sind 'kleinteilig' und so detailiert, daß der menschliche Leser schnell den Überblick verliert (daher natürlich-sprachliche Beweise in Mathematikbüchern). Angefangen hat das Ende der 50er Jahre des letzten Jahrhunderts mit dem "Logical Theorist" von Newell und Simon.

5) Welche Problematik meinst Du?

Wenn Du Dich für das Arbeiten mit Beweisassistenten interessierst, dann schau mal unter http://verifun.de . Die Sprache des dortigen Systems ist nicht so ausdrucksstark wie etwa bei COQ oder Lean, das Prädikatenlogikbeispiel kann man damit nicht bearbeiten. Dafür ist das System aber leichter erlern- und bedienbar. Man kann damit Programme, wie etwa Sortieralgorithmen, verifizieren, Beweise aus der Zahlentheorie führen, die Unentscheidbarkeit des Halteproblems nachweisen, usw.



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.7, vom Themenstarter, eingetragen 2019-07-12



2) Ohne den Ebbinghaus jetzt zur Hand zu haben gehe ich fest davon aus, daß Terme und Formeln dort natürlich-sprachlich definiert werden (und bestimmt nicht mittels des Kleenschen Fixpunktsatzes, den man dafür überhaupt nicht braucht).

Du schreibst: "eine implizite Forderung an  metasprachliche Definitionen ist jedoch, daß diese einfach und allgemein als verständlich anerkannt sind."
Zu "einfach und allgemein als verständlich". Damit habe ich ein Problem:
Definition der Terme in der Metasprache  bei Ebbinghaus:
S-Terme sind genau diejenigen Zeichenreihen welche man durch endlichmalige Anwendung der folgenden Regeln erhalten kann:
(T1) Jede Variable ist ein Term
(T2) ….
(T3) …

Diese Definition wurde in der Vorlesung von Schwabhäuser als unpräzise bezeichnet.
(vor allem die Bezeichnung „kann“)
Definition der Terme in der Metasprache bei Schwabhäuser:
T  ist ein Term <==> es existiert eine endliche Folge( t_0, …, t_n) von Zeichenreihen so dass t_n = T und für alle 1<= i <=n gilt: t_i ist eine Variable oder t_i entsteht aus früheren Gliedern der Folge durch Anwendung einer der Schlussregeln (T2) oder (T3)

Es kann also verschiedene Auffassungen über "einfach und allgemein als verständlich" geben.
Außerdem finde eine induktive Definition nicht einfach (durch ein "falsche" Definition könnte es eine "Endlosschleife" geben) . Deswegen wird eine induktive Definition ja durch induktiv definierte Mengen formalisiert bzw. das steckt dahinter. Sobald also eine Präzisierung erfolgt (wie z.B. durch eine induktiv definierte Menge) wird die Anforderung "einfach" nicht mehr erfüllt.


3) Tatsächlich findet man in mathematischen Aufsätzen um die 30er Jahre des letzten Jahrhunderts Kapitel, in denen zunächst bewiesen wird, daß man von der Existenz abzählbarer Mengen von Variablensymbolen, Funktionssymbolen usw. tatsächlich ausgehen darf.
Damit verwendet man etwas, was also metasprachlich nicht so "einfach" ersichtlich ist, bzw. erst einmal in der Metasprache "bewiesen" werden muss.
Wie präzise ist aber ein metasprachlicher (und damit informaler) Beweis. Was gibt mir die Sicherheit, dass er "korrekt" ist ?


4) Das Problem war, wie aussagekräftig Ergebnisse der Mathematik sind, wenn deren Nachweis lediglich informell, also nicht-mathematisch ist. Ergebnis war die Formalisierung des mathematischen Schließens ...
Die Formale Logik wurde als Werkzeug entwickelt, um Aussagen ÜBER das mathematische Schließen zu treffen ...

Ich nehme mal als Beispiel den Satz "Korrektheit der Schlussregeln", speziell:
Aus der Schlussregel a, a->b, b folgt:
Aus I |= a und I |= a->b folgt I  |= b    (I ist eine Interpretation).
Hier ein metasprachlicher Beweis:
Es sei I |= a und es sei I |= a->b
I |= a->b bedeutet:
Wenn I |= a, dann I |= b
Da aber  I |= a gilt, folgt I |= b

Wo wird hier (im metasprachlichen Beweis) die "formale Logik" als "Werkzeug" benutzt ?
Was hat das mit der "Formalisierung des mathematischen Schließens" zu tun ?
Das versteh ich nicht. In diesem Beweis benutze ich (im Subtext, also ohne sie zu erwähnen, was auch in allen Mathebüchern so gemacht wird) viele metasprachliche Regeln, die nirgendwo spezifiziert werden.
Deswegen habe ich immer noch das Problem:
wie "aussagekräftig" ist der Satz ("Korrektheit der Schlussregeln") bzw. dessen zugehöriger Beweis , wenn der Beweis lediglich informell, also nicht-mathematisch ist?
Die „Formalisierung des mathematischen Schließen“ hilft mir hier auch nicht weiter, das sie nur FOL betrifft und nicht metasprachliche Beweise (wie z.B. den metasprachlichen Beweis vom Satz "Korrektheit der Schlussregeln").

3)
Zum Standardmodell der natürlichen Zahlen.
Ich bastle wie folgt ein Standarmodell
a) Die Trägermenge N0
N0 := {0, 1, 2, ..., 9}
mit 0 < 1 < 2 < ... <9

N ist die Menge aller endlichen Folgen, deren Folgenglieder jeweils aus Elementen aus N0 besteht.
Damit ist (1,2,3) abgekürzt durch 123 Element von N
b) Definition der Addition +
0 + 0 := 0
...
9 + 9 := 18

n_1 ... n_m + p_1 ... p_q := siehe Algorithmus aus der Grundschule
oder Implementierung des ADD Befehls in der CPU (ALU)

c) Multiplikation analog

Warum macht man das nicht so?
Das wäre doch ziemlich "einfach", oder ?

mfg
cx















  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 190
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.8, eingetragen 2019-07-13


2019-07-12 15:41 - carlox in Beitrag No. 7 schreibt:

2) Ohne den Ebbinghaus jetzt zur Hand zu haben gehe ich fest davon aus, daß Terme und Formeln dort natürlich-sprachlich definiert werden (und bestimmt nicht mittels des Kleenschen Fixpunktsatzes, den man dafür überhaupt nicht braucht).

Du schreibst: "eine implizite Forderung an  metasprachliche Definitionen ist jedoch, daß diese einfach und allgemein als verständlich anerkannt sind."
Zu "einfach und allgemein als verständlich". Damit habe ich ein Problem:
Definition der Terme in der Metasprache  bei Ebbinghaus:
S-Terme sind genau diejenigen Zeichenreihen welche man durch endlichmalige Anwendung der folgenden Regeln erhalten kann:
(T1) Jede Variable ist ein Term
(T2) ….
(T3) …

Diese Definition wurde in der Vorlesung von Schwabhäuser als unpräzise bezeichnet.
(vor allem die Bezeichnung „kann“)
Definition der Terme in der Metasprache bei Schwabhäuser:
T  ist ein Term <==> es existiert eine endliche Folge( t_0, …, t_n) von Zeichenreihen so dass t_n = T und für alle 1<= i <=n gilt: t_i ist eine Variable oder t_i entsteht aus früheren Gliedern der Folge durch Anwendung einer der Schlussregeln (T2) oder (T3)

Es kann also verschiedene Auffassungen über "einfach und allgemein als verständlich" geben.
Außerdem finde eine induktive Definition nicht einfach (durch ein "falsche" Definition könnte es eine "Endlosschleife" geben) . Deswegen wird eine induktive Definition ja durch induktiv definierte Mengen formalisiert bzw. das steckt dahinter. Sobald also eine Präzisierung erfolgt (wie z.B. durch eine induktiv definierte Menge) wird die Anforderung "einfach" nicht mehr erfüllt.

"Einfach und allgemein verständlich" bezieht sich auf Personen mit fundiertem mathematischem Hintergrund, und nicht etwa auf Studenten in niedrigen Semestern oder Leute, die beginnen sich mit der Materien vertraut zu machen.

Beide Definitionen von Termen sind in diesem Sinne "einfach und allgemein verständlich", wobei nicht ausgeschlossen ist, daß es durchaus unterschiedliche Ansichten geben kann, welche von beiden "einfacher" ist. Ist die eine für mich "einfacher" als die andere, so heißt das ja nicht notwendigerweise, daß die andere nicht einfach ist.

Für mich ist das Induktionsprinzip (und damit das Rekursionsprinzip) einfach. Die zugrunde liegende Mathematik ist keineswegs schwer und kompliziert.

In der Mathematik gibt es keine Schleifen. Definiere ich in der Arithmetik f(x) = f(x) + 1, so erhalte ich die überall undefinierte Funktion. Schreibe ich statt dessen f(x) = f(x + 1), so erhalte ich eine Konstante (deren genauer Wert verborgen bleibt).  

PS: Die Kritik an "kann" halte ich für eine alberne Korinthenkackerei, mal abgesehen davon daß die Definition dadurch nicht "unpräzise" ist. Die andere Definition ist nicht präziser sondern falsch: Man muß "0 <= i <= n" schreiben, sonst ist jeder Ausdruck ein Term.
   



3) Tatsächlich findet man in mathematischen Aufsätzen um die 30er Jahre des letzten Jahrhunderts Kapitel, in denen zunächst bewiesen wird, daß man von der Existenz abzählbarer Mengen von Variablensymbolen, Funktionssymbolen usw. tatsächlich ausgehen darf.
Damit verwendet man etwas, was also metasprachlich nicht so "einfach" ersichtlich ist, bzw. erst einmal in der Metasprache "bewiesen" werden muss. Wie präzise ist aber ein metasprachlicher (und damit informaler) Beweis. Was gibt mir die Sicherheit, dass er "korrekt" ist ?

Es gibt in diesem Leben keine abolute Sicherheit, nie und nirgends. Informelle Definitionen und Beweise haben den Vorteil, daß sie für den menschlichen Leser sehr viel verständlicher sind, als formale Definitionen und Beweise. Letztere haben bei Verwendung von Computern (Beweisassistenten, Proofchecker) den Vorteil, daß fehlerhafte Schlußweisen vermieden bzw. erkannt werden, was bei informellen Definitionen und Beweisen nicht möglich ist. Eine absolute Sicherheit hat man hier jedoch auch nicht, die Programme können fehlerhaft sein, die verwendete Programmiersprache kann fehlerhaft implementiert sein, die zugrunde liegende Hardware kann fehlerhaft sein. Nur wird man das irgendwann bemerken, reparieren und bislang errechnete Resultate dann überprüfen (schau mal im Internet nach dem "Pentium Bug" als Beispiel).  



4) Das Problem war, wie aussagekräftig Ergebnisse der Mathematik sind, wenn deren Nachweis lediglich informell, also nicht-mathematisch ist. Ergebnis war die Formalisierung des mathematischen Schließens ...
Die Formale Logik wurde als Werkzeug entwickelt, um Aussagen ÜBER das mathematische Schließen zu treffen ...

Ich nehme mal als Beispiel den Satz "Korrektheit der Schlussregeln", speziell:
Aus der Schlussregel a, a->b, b folgt:
Aus I |= a und I |= a->b folgt I  |= b    (I ist eine Interpretation).
Hier ein metasprachlicher Beweis:
Es sei I |= a und es sei I |= a->b
I |= a->b bedeutet:
Wenn I |= a, dann I |= b
Da aber  I |= a gilt, folgt I |= b

Wo wird hier (im metasprachlichen Beweis) die "formale Logik" als "Werkzeug" benutzt ?
Was hat das mit der "Formalisierung des mathematischen Schließens" zu tun ?
Das versteh ich nicht. In diesem Beweis benutze ich (im Subtext, also ohne sie zu erwähnen, was auch in allen Mathebüchern so gemacht wird) viele metasprachliche Regeln, die nirgendwo spezifiziert werden.
Deswegen habe ich immer noch das Problem:
wie "aussagekräftig" ist der Satz ("Korrektheit der Schlussregeln") bzw. dessen zugehöriger Beweis , wenn der Beweis lediglich informell, also nicht-mathematisch ist?
Die „Formalisierung des mathematischen Schließen“ hilft mir hier auch nicht weiter, das sie nur FOL betrifft und nicht metasprachliche Beweise (wie z.B. den metasprachlichen Beweis vom Satz "Korrektheit der Schlussregeln").

Das habe ich schon in #6 beantwortet. Man wird die informelle, in natürlicher Sprache formulierte, Mathematik letztendlich nie los. Diese Kröte muß man eben schlucken, da hilft kein lamentieren.
 

3) Zum Standardmodell der natürlichen Zahlen.
Ich bastle wie folgt ein Standarmodell
a) Die Trägermenge N0
N0 := {0, 1, 2, ..., 9}
mit 0 < 1 < 2 < ... <9

N ist die Menge aller endlichen Folgen, deren Folgenglieder jeweils aus Elementen aus N0 besteht.
Damit ist (1,2,3) abgekürzt durch 123 Element von N
b) Definition der Addition +
0 + 0 := 0
...
9 + 9 := 18

n_1 ... n_m + p_1 ... p_q := siehe Algorithmus aus der Grundschule
oder Implementierung des ADD Befehls in der CPU (ALU)

c) Multiplikation analog

Warum macht man das nicht so?
Das wäre doch ziemlich "einfach", oder ?

Ob das einfach ist kann ich jetzt nicht sagen, das müßte man dann schon ausarbeiten. Aber mal unterstellt, es wäre einfach. Was würde dann daraus folgen, welche Erkenntnisse brächte das dann?



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.9, vom Themenstarter, eingetragen 2019-07-14


Hallo ZA,

In der Mathematik gibt es keine Schleifen. Definiere ich in der Arithmetik f(x) = f(x) + 1, so erhalte ich die überall undefinierte Funktion. Schreibe ich statt dessen f(x) = f(x + 1), so erhalte ich eine Konstante (deren genauer Wert verborgen bleibt).  

Ich weiß, dass es in der Mathematik keine Schleifen gibt.
Ich wollte damit abkürzend sagen, dass eine unsachgemäße rekursive Definition nicht das abbildet, was man eigentlich abbilden will.
Deshalb muss man z.B. aufpassen, dass eine Rekursion irgendwann "endet".


PS: Die Kritik an "kann" halte ich für eine alberne Korinthenkackerei, mal abgesehen davon daß die Definition dadurch nicht "unpräzise" ist. Die andere Definition ist nicht präziser sondern falsch: Man muß "0 <= i <= n" schreiben, sonst ist jeder Ausdruck ein Term.
Das war ein Schreibfehler von mir. Den habe _ich_ zu verantworten.


Das habe ich schon in #6 beantwortet. Man wird die informelle, in natürlicher Sprache formulierte, Mathematik letztendlich nie los. Diese Kröte muß man eben schlucken, da hilft kein lamentieren.
Habe kein Problem, dass man "die informelle, in natürlicher Sprache formulierte, Mathematik letztendlich nie los wird".
Angenommen, man formalisert einen metasprachlichen Beweis so weit wie möglich.
Dann habe ich folgende Kritik:
Warum werden die Regeln, Schlussweisen usw., die man in metasprachlichen Beweisen verwendet, _nirgends_ angegeben?
Konkrtet:
Warum wird z.B. die folgende metasprachliche Schlussregel:

A, A ==> B
----------
B

und weitere - wenigstens ein einziges Mal - explizit z.B. am Anfang eines Mathematikbuchs irgendwo notiert (so wie es z.B. in FOL gemacht wird).
Zumindest Ebbinghaus (Einführug in die Mengenlehre) spricht dieses Thema an:
"Analog nennen wir die Definition 3.3 eine Definition durch metasprachliche Induktion"


Ob das einfach ist kann ich jetzt nicht sagen, das müßte man dann schon ausarbeiten. Aber mal unterstellt, es wäre einfach. Was würde dann daraus folgen, welche Erkenntnisse brächte das dann?

Für mich ist dieses von mir skizzierte Standardmodell doch das, was man in der Grundschule verwendet. Es ist das natürlichste, intuitivste Standardmodell, weil es jedem Menschen, der mit Zahlen zu tun hat, bekannt ist.
Ebbinghaus spricht von den naiven Zahlen.
Warum wird es nicht verwendet ?

mfg
cx









  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 190
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.10, eingetragen 2019-07-15


2019-07-14 09:17 - carlox in Beitrag No. 9 schreibt:
Hallo ZA,

In der Mathematik gibt es keine Schleifen. Definiere ich in der Arithmetik f(x) = f(x) + 1, so erhalte ich die überall undefinierte Funktion. Schreibe ich statt dessen f(x) = f(x + 1), so erhalte ich eine Konstante (deren genauer Wert verborgen bleibt).  

Ich weiß, dass es in der Mathematik keine Schleifen gibt.
Ich wollte damit abkürzend sagen, dass eine unsachgemäße rekursive Definition nicht das abbildet, was man eigentlich abbilden will.
Deshalb muss man z.B. aufpassen, dass eine Rekursion irgendwann "endet".

In meinen beiden Beispielen endet die Rekursion nicht, trotzdem sind die Definitionen sinnvoll. Aber das sind Sonderfälle, i.A. hast Du schon recht. Aber: Ob das, was man hingeschrieben hat auch das ist, was man gemeint hat, ist generell nicht überprüfbar, das ist auch bei nicht rekursiven Definitionen so.
 


PS: Die Kritik an "kann" halte ich für eine alberne Korinthenkackerei, mal abgesehen davon daß die Definition dadurch nicht "unpräzise" ist. Die andere Definition ist nicht präziser sondern falsch: Man muß "0 <= i <= n" schreiben, sonst ist jeder Ausdruck ein Term.
Das war ein Schreibfehler von mir. Den habe _ich_ zu verantworten.

Woran man sieht, daß das geschulte Auge auch Fehler in informellen Definitionen erkennen kann :-)



Das habe ich schon in #6 beantwortet. Man wird die informelle, in natürlicher Sprache formulierte, Mathematik letztendlich nie los. Diese Kröte muß man eben schlucken, da hilft kein lamentieren.

Habe kein Problem, dass man "die informelle, in natürlicher Sprache formulierte, Mathematik letztendlich nie los wird".
Angenommen, man formalisert einen metasprachlichen Beweis so weit wie möglich.
Dann habe ich folgende Kritik:
Warum werden die Regeln, Schlussweisen usw., die man in metasprachlichen Beweisen verwendet, _nirgends_ angegeben?
Konkrtet:
Warum wird z.B. die folgende metasprachliche Schlussregel:

A, A ==> B
----------
B

und weitere - wenigstens ein einziges Mal - explizit z.B. am Anfang eines Mathematikbuchs irgendwo notiert (so wie es z.B. in FOL gemacht wird).

Weil man das nicht braucht. Ich habe es nie vermißt, und bin dabei offenbar nicht alleine.



Ob das einfach ist kann ich jetzt nicht sagen, das müßte man dann schon ausarbeiten. Aber mal unterstellt, es wäre einfach. Was würde dann daraus folgen, welche Erkenntnisse brächte das dann?

Für mich ist dieses von mir skizzierte Standardmodell doch das, was man in der Grundschule verwendet. Es ist das natürlichste, intuitivste Standardmodell, weil es jedem Menschen, der mit Zahlen zu tun hat, bekannt ist.
Ebbinghaus spricht von den naiven Zahlen.
Warum wird es nicht verwendet ?

Weil es im Unterschied zu dem klassischen Ansatz (natürliche Zahlen repräsentiert durch endlichmalige Anwendung der Nachfolgerfunktion S auf die 0 plus die Peano-Axiome) wesentlich komplizierter ist.

Wenn man wie üblich

all y.     0 + y = y
all x, y. S(x) + y = S(x + y)

definiert, dann ist z.B der Beweis der Assozitivität von + ein so trivialer Peano-Induktionsbeweis, daß das nicht einmal für eine Klausuraufgabe taugt.

Jetzt nimm Dir eine Programmiersprache Deiner Wahl, implementier darin Deinen Ansatz und beweise anschließend die Assozitivität der Addition nach Deiner Definition. Du kannst auch irgendeinen Beweisassistenten dazu verwenden. Egal wie Du es machst, Du wirst feststellen, daß der Beweis bei weitem nicht einfach ist und die Intuition verloren geht, wenn andere den Beweis nachvollziehen wollen.



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.11, vom Themenstarter, eingetragen 2019-07-15



Habe kein Problem, dass man "die informelle, in natürlicher Sprache formulierte, Mathematik letztendlich nie los wird".
Angenommen, man formalisert einen metasprachlichen Beweis so weit wie möglich.
Dann habe ich folgende Kritik:
Warum werden die Regeln, Schlussweisen usw., die man in metasprachlichen Beweisen verwendet, _nirgends_ angegeben?
Konkrtet:
Warum wird z.B. die folgende metasprachliche Schlussregel:

A, A ==> B
----------
B

und weitere - wenigstens ein einziges Mal - explizit z.B. am Anfang eines Mathematikbuchs irgendwo notiert (so wie es z.B. in FOL gemacht wird).

Weil man das nicht braucht. Ich habe es nie vermißt, und bin dabei offenbar nicht alleine.

Es gibt doch die Russelsche Antinomie - Widersprüche in der naiven Mengenlehre.
Das zeigt doch, dass es sinnvoll ist, alle Hilfsmittel, Schlussweisen, usw. in der Metasprache anzugeben und zu formulieren.


Für mich ist dieses von mir skizzierte Standardmodell doch das, was man in der Grundschule verwendet. Es ist das natürlichste, intuitivste Standardmodell, weil es jedem Menschen, der mit Zahlen zu tun hat, bekannt ist.
Ebbinghaus spricht von den naiven Zahlen.
Warum wird es nicht verwendet ?

Weil es im Unterschied zu dem klassischen Ansatz (natürliche Zahlen repräsentiert durch endlichmalige Anwendung der Nachfolgerfunktion S auf die 0 plus die Peano-Axiome) wesentlich komplizierter ist.

Wenn man wie üblich

all y.     0 + y = y
all x, y. S(x) + y = S(x + y)

definiert, dann ist z.B der Beweis der Assozitivität von + ein so trivialer Peano-Induktionsbeweis, daß das nicht einmal für eine Klausuraufgabe taugt.

Jetzt nimm Dir eine Programmiersprache Deiner Wahl, implementier darin Deinen Ansatz und beweise anschließend die Assozitivität der Addition nach Deiner Definition. Du kannst auch irgendeinen Beweisassistenten dazu verwenden. Egal wie Du es machst, Du wirst feststellen, daß der Beweis bei weitem nicht einfach ist und die Intuition verloren geht, wenn andere den Beweis nachvollziehen wollen.

Ich nenne das von dir angegebene Standardmodell das einfache Standardmodell (ESM)
Das von mir skizzierte Standardmodell nenne ich das das naive Standardmodell (NSM).
Zugegeben, die Beweise im ESM sind einfacher.
Aber man kommt nicht umhin, zu zeigen, dass ESP und NSM äquivalent sind.
Sonst wäre ja das ganze Rechnen in der Grundschule nicht gerechtfertigt.
D.h. diesen Beweis kann man nicht unterschlagen. Man kommt also nicht an ihm und an NSM vorbei.

mfg
cx
 




  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 190
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.12, eingetragen 2019-07-15


2019-07-15 19:22 - carlox in Beitrag No. 11 schreibt:
Es gibt doch die Russelsche Antinomie - Widersprüche in der naiven Mengenlehre. Das zeigt doch, dass es sinnvoll ist, alle Hilfsmittel, Schlussweisen, usw. in der Metasprache anzugeben und zu formulieren.

Genaugenommen zeigt es das Gegenteil: Die Antinomien hat man ja OHNE Angabe von Schlußweisen in der Metasprache erkannt und eliminiert.

2019-07-15 19:22 - carlox in Beitrag No. 11 schreibt:

Ich nenne das von dir angegebene Standardmodell das einfache Standardmodell (ESM)
Das von mir skizzierte Standardmodell nenne ich das das naive Standardmodell (NSM).
Zugegeben, die Beweise im ESM sind einfacher.
Aber man kommt nicht umhin, zu zeigen, dass ESP und NSM äquivalent sind.

Natürlich kann man diese Äquivalenz beweisen. Aber darum geht es nicht. Deine Behauptung war das NSM einfacher und intuitiver ist als ESM, und das stimmt eben nicht, wenn man Beweise in der Arithmetik führen will.




  Profil  Quote  Link auf diesen Beitrag Link
smirk_mirkin
Junior Letzter Besuch: in der letzten Woche
Dabei seit: 04.12.2014
Mitteilungen: 17
Aus: Leipzig, Deutschland
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.13, eingetragen 2019-07-16


Lieber Carlox, angesichts dessen, dass mich derlei Fragen auch umgetrieben haben und das nun zu einem beginnenden Logikstudium geführt hat, werde ich einen Antwortversuch wagen.


2) Du meinst die Definition von Termen und Formel in der Metasprache.
Terme und Formeln werden mit induktiv definierten Mengen (deren Grundlage die Mengenlehre ist) formalisiert. Dahinter steckt der Kleensche Fixpunktsatz.
Induktiv definierten Mengen (und die Mengenlehre) sind aber alles andere als " einfach und allgemein verständlich".
Was meinst du dazu ?

Eine Definition kann verständlich sein, auch wenn die für ihre nähere formale Analyse benötigte Mathematik nicht-trivial ist. Genau das ist hier der Fall: Zum Verständnis "benötigt" man nur die Konzepte "Zeichenkette", "Menge", "Regelanwendung", in der Folge kann man prüfen, ob eine Zeichenkette die Definition erfüllt.


3) Das fängt schon viel früher an:
Bei der Definition der Syntax [...] muss [das] ja eine natürliche Sprache wie z.B. Englisch oder Deutsch sein.

4) Beweisbarkeit in der Metasprache formulieren.
Bei einem "normalen" mathemtischem Beweis (also nicht der formale Ableitungsbegriff in der Prädikatenlogik) werden stillschweigend Annahmen (Schlussregeln, usw.) getroffen und benutzt, die die nirgends in der Metasprache spezifiziert werden (ist eigentlich intellektuell unredlich).
Ein in der Metasprache angegebener Beweis ist m.M. nach ähnlich einem Beweis in FOL. Nur ist ein FOL-Beweis formal spezifiziert.

Wir benutzen für derlei Dinge meiner Meinung nach NICHT ausschließlich natürliche Sprache. Wir benutzen die (moderne) mathematische Fachsprache. Diese basiert bereits "im Hintergrund" auf einer Logik und einer Mengenlehre. Wenn wir nun Beweise führen, so tun wir das informell, beziehen uns dabei jedoch auf Schlussregeln unserer Metalogik. Welche diese Metalogik ist, ist hingegen nicht so leicht zu beantworten. In der Regel wird es Prädikatenlogik höherer Stufe sein. Dieser Ansatz hat den großen Vorteil, dass er verständlicher ist als formale Logik, aber sicherer als reine natürliche Sprache. Er vereint die Vorteile aus beidem und macht so das Mathematiktreiben erst möglich.

Um unsere Mathematik auf dieser Basis abzusichern, kann man die Logik formal untersuchen. Das geschieht z.B. in Ebbinghaus/Flum/Thomas. Dort entwirft man mit Kalkülen ein strenges Beweismodell, mithilfe dessen man ganz formal die Beweise der Mathematik nachbilden kann. Die Erkenntnisse, die man so gewinnt, kann man dann natürlich auch auf die Metasprache mit ihrer Metalogik anwenden.


Ich nehme mal als Beispiel den Satz "Korrektheit der Schlussregeln", speziell:
Aus der Schlussregel a, a->b, b folgt:
Aus I |= a und I |= a->b folgt I  |= b    (I ist eine Interpretation).
Hier ein metasprachlicher Beweis:
Es sei I |= a und es sei I |= a->b
I |= a->b bedeutet:
Wenn I |= a, dann I |= b
Da aber  I |= a gilt, folgt I |= b

Wo wird hier (im metasprachlichen Beweis) die "formale Logik" als "Werkzeug" benutzt ?

Also erstmal verstehe ich nicht vollständig, was du tust. Aus einer Schlussregel folgt gar nichts. Wir haben diese Schlussregel mit einer gewissen Intention entworfen und wollen nun prüfen, ob sie dieser Intention standhält. Genauer: Wir prüfen, ob sie mit der Folgerungsbeziehung aus der Logik verträglich ist.

Sei also I Modell von a und a->b. Dann folgt aus der Semantik-Definition von -> sofort, dass I auch Modell für b ist. Also ist b eine Folgerung von {a, a->b}.

Der gesamte Beweis findet auf der Ebene der Metasprache statt. Wie man an dem Wörtchen "folgt" gut sieht, besitzt diese Metasprache eine Metalogik mit einem ganz eigenen Folgerungsbegriff, der von dem nachfolgenden Begriff "Folgerung" hier unabhängig ist. Da diese Metalogik hier ebenfalls eine Logik erster Stufe ist, gelten die bei der Untersuchungen zutage geförderten Zusammenhänge natürlich auch für sie selbst.


"Einfach und allgemein verständlich" bezieht sich auf Personen mit fundiertem mathematischem Hintergrund, und nicht etwa auf Studenten in niedrigen Semestern oder Leute, die beginnen sich mit der Materien vertraut zu machen.

Diese Relativierung halte ich nicht für nötig. Lass dich doch nicht so einfach in die Flucht schlagen, lieber Zwerg_Allwissend  smile


PS: Die Kritik an "kann" halte ich für eine alberne Korinthenkackerei [...]

Ich auch, im wesentlichen sind beide Definitionen gleich. Die Zweite versucht eher unnötig die "endliche Regelanwendung" zu präzisieren.


Wie präzise ist aber ein metasprachlicher (und damit informaler) Beweis. Was gibt mir die Sicherheit, dass er "korrekt" ist ?

Anknüpfend an das oben Gesagte: Man kann davon ausgehen, dass sich unsere informellen Beweise auch formal-logisch formulieren lassen, wenn man sich an gewisse Spielregeln hält. Ob das im Einzelfall so ist: siehe Antwort #6 von Zwerg_Allwissend. Da man beim Mathematik-Studium aber genau diese Sprache einübt ist das eher kein kritischer Punkt.


Es gibt doch die Russelsche Antinomie - Widersprüche in der naiven Mengenlehre.
Das zeigt doch, dass es sinnvoll ist, alle Hilfsmittel, Schlussweisen, usw. in der Metasprache anzugeben und zu formulieren.

*** Überarbeitete Antwort ***

Zugegeben habe ich die Aussage bei nochmaligem Durchlesen nicht ganz verstanden. Die Hilfsmittel sind impliziter Natur (man benutzt die Standard-Metasprache der Mathematik) und die Schlussweisen entsprechen ja gerade dem Beweis mit seinen einzelnen Schritten.

Deutet man deine Aussage eher so, dass man formaler arbeiten sollte, um keine Paradoxien entstehen zu lassen, so ist das nicht notwendig.

Die Paradoxien zeigten, dass eine Reflexion über die Grundlagen der Mathematik und ihre Spielregeln sinnvoll ist. Diese ist aber prinzipieller Natur und erfolgt über die entsprechenden Teildisziplinen (Logik, Mengenlehre) und die Philosophie der Mathematik. Historisch ist man durch diese Reflexion auf Grenzen gestoßen: Die Utopie eines umfassenden, in sich geschlossenen und abgesicherten mathematischen Ökosystems ist leider unhaltbar.

Andererseits treten Paradoxien erst auf, sobald man aus bekannten Anschauungsräumen heraus tritt. Z.B. tief im Unendlichen und bei sehr exotischen Mengenbildungen.


Genau genommen zeigt es das Gegenteil: Die Antinomien hat man ja OHNE Angabe von Schlußweisen in der Metasprache erkannt und eliminiert.

Das ist falsch. Die Antinomien wurden vor allem bei der Formalisierung des mathematischen Schließens in Kalkülen entdeckt. Die Russellsche Antinomie beispielsweise in Freges Kalkül.


Nachtrag zur Diskussion bzgl. des Standardmodells:


Warum macht man das nicht so?
Das wäre doch ziemlich "einfach", oder ?

Was bedeutet denn "man" und "das"?
WAS soll MAN so machen?


Für mich ist dieses von mir skizzierte Standardmodell doch das, was man in der Grundschule verwendet. Es ist das natürlichste, intuitivste Standardmodell, weil es jedem Menschen, der mit Zahlen zu tun hat, bekannt ist.
Ebbinghaus spricht von den naiven Zahlen.
Warum wird es nicht verwendet ?

Es wird doch verwendet, jeder lernt es bereits in der Grundschule.


Aber man kommt nicht umhin, zu zeigen, dass ESP und NSM äquivalent sind.

Das ist intuitiv klar und formal nicht besonders schwer.
Es handelt sich nur um verschiedene Darstellungen der natürlichen Zahlen.
Zum einen werden Zahlensysteme regelmäßig behandelt, zum anderen muss man eben nicht die gesamte Theorie zu den Fundamenten der Mathematik behandeln, um Mathematik zu treiben.

Interessant ist hierbei eher wieder der Meta-Blickwinkel:

- Wie stehen Peano-Strukturen und das Standardmodell der Zahlen zueinander? Gibt es nicht-isomorphe sonstige Modelle?
- Was sind verschiedene Darstellungen der natürlichen Zahlen? Sind es nur (Meta-)Darstellungen um über ein und dieselbe Struktur zu reden? Oder sind es verschiedene aber isomorphe Strukturen?



  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 190
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.14, eingetragen 2019-07-16


2019-07-16 10:00 - smirk_mirkin in Beitrag No. 13 schreibt:

"Einfach und allgemein verständlich" bezieht sich auf Personen mit fundiertem mathematischem Hintergrund, und nicht etwa auf Studenten in niedrigen Semestern oder Leute, die beginnen sich mit der Materien vertraut zu machen.

Diese Relativierung halte ich nicht für nötig. Lass dich doch nicht so einfach in die Flucht schlagen, lieber Zwerg_Allwissend  smile

So hatte ich es aber gemeint. "Verstehen" ist nicht nur eine intellektuelle Herausforderung, sondern auch von Vorkenntnissen abhängig. Extrembeispiel: Den Beweis des "Großen Fermat" von Wiles et. al. verstehen vielleicht zwei Dutzend Mathematiker, der Rest nicht (was ja nicht heißt, daß der Rest dumm und ungebildet ist). Wohl jeder, der beginnt sich mit der Materie zu beschäftigen, hat Verständnisschwierigkeiten. Kurzum, auch Zwerge haben klein angefangen!  



Genau genommen zeigt es das Gegenteil: Die Antinomien hat man ja OHNE Angabe von Schlußweisen in der Metasprache erkannt und eliminiert.

Das ist falsch. Die Antinomien wurden vor allem bei der Formalisierung des mathematischen Schließens in Kalkülen entdeckt. Die Russellsche Antinomie beispielsweise in Freges Kalkül.

Warum ist meine Behauptung falsch? Du schreibst doch selbst "vor allem bei der Formalisierung des mathematischen Schließens in Kalkülen entdeckt", also eben nicht mittels "Schlußweisen in der Metasprache".

Ansonsten: Gut gebrüllt, Löwe!



  Profil  Quote  Link auf diesen Beitrag Link
smirk_mirkin
Junior Letzter Besuch: in der letzten Woche
Dabei seit: 04.12.2014
Mitteilungen: 17
Aus: Leipzig, Deutschland
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.15, eingetragen 2019-07-16


2019-07-16 13:55 - Zwerg_Allwissend in Beitrag No. 14 schreibt:
So hatte ich es aber gemeint. "Verstehen" ist nicht nur eine intellektuelle Herausforderung, sondern auch von Vorkenntnissen abhängig. Extrembeispiel: Den Beweis des "Großen Fermat" von Wiles et. al. verstehen vielleicht zwei Dutzend Mathematiker, der Rest nicht (was ja nicht heißt, daß der Rest dumm und ungebildet ist). Wohl jeder, der beginnt sich mit der Materie zu beschäftigen, hat Verständnisschwierigkeiten. Kurzum, auch Zwerge haben klein angefangen!

Da stimme ich dir zu. Es wirkte nur so, als hättest du dich im Nachhinein auf dieses "speziellere"  Konzept von Einfachheit zurückgezogen. Aber in dem konkreten Fall, bei der Definition der Logik, benötigt man für das Verständnis eben wirklich nur elementare Konzepte. Und ich finde es an der Stelle auch wichtig das hervorzuheben.

2019-07-16 13:55 - Zwerg_Allwissend in Beitrag No. 14 schreibt:

Warum ist meine Behauptung falsch? Du schreibst doch selbst "vor allem bei der Formalisierung des mathematischen Schließens in Kalkülen entdeckt", also eben nicht mittels "Schlußweisen in der Metasprache".

Dann habe ich dich hier falsch verstanden.

Die Entwicklung von entsprechenden Kalkülen ist ja gerade das Formalisieren von Schlussweisen der Metasprache. Damit wurden dann auch einige Paradoxien der Mengenlehre(n) aufgedeckt. Also hat man diese DURCH die Untersuchung der metasprachlichen Schlussweisen aufgedeckt. Vielleicht hast du das ja auch so ähnlich gemeint?

Jedenfalls zeigt uns das, dass es natürlich geboten ist, die Sprache und deren Möglichkeiten zu reflektieren. Aber eben nicht, dass man sie gänzlich aufgeben sollte.



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.16, vom Themenstarter, eingetragen 2019-07-17


Hallo smirk_mirkin,

... auch umgetrieben haben und das nun zu einem beginnenden Logikstudium geführt hat, werde ich einen Antwortversuch wagen.
Das interessiert mich:
Gibt es ein reines Logikstudium oder ist das in ein anderes Studium eingebettet ?
Wo kann man das studieren ?
Gibt es dazu Infos (z.B. über die Vorlesungen) ?


...Wenn wir nun Beweise führen, so tun wir das informell, beziehen uns dabei jedoch auf Schlussregeln unserer Metalogik. Welche diese Metalogik ist, ist hingegen nicht so leicht zu beantworten. In der Regel wird es Prädikatenlogik höherer Stufe sein.
Gut, dass ich jetzt auch nicht alleine bin (Zitat ZA:
"Weil man das nicht braucht. Ich habe es nie vermißt, und bin dabei offenbar nicht alleine.")
Hätte mich bei einem Logikstudium auch gewundert, dass man das ausblendet.
Ich versuche mal konkret zu werden, weil ich sonst nicht weiss, ob wir noch von der gleichen Sache reden.

Fall1: Satz ist in FOL formulierbar
Beispiel: PA bedeuten die Peano-Axiome .
Man will z.B. zeigen, dass in allen Modellen gilt:
x=0 und y=0 ==> x+y=0
Man will also zeigen:
$PA \models x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow
x \oplus y \equiv \overline{0} $
Nach dem Vollständigkeitssatz genügt zu zeigen:
$PA \vdash x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow
x \oplus y \equiv \overline{0} $
Ok, jetzt ist man auf FOL-Ebene mit den FOL-Schlussregeln und kann dann einen Beweis in FOL machen.

Fall2: Satz ist nicht in FOL formulierbar
Beispiel:
$\quad \Sigma \vdash \varphi \implies \Sigma \models \varphi$
Den Beweis kann man jetzt nicht mehr auf FOL-Ebene machen.
man braucht eine Metalogik.
Welche ? Prädikatenlogik 2. Stufe ?

Fall3: Satz ist nicht in FOL formulierbar
Beispiel:
Alle ganzen, natürlichen Zahlen grösser 2 sind im Standardmodell von PA als Summe zweier Primzahlen darstellbar.
Angenommen der Satz ist wahr.
Der Beweis ist nicht mehr auf FOL-Ebene machbar.
man braucht eine Metalogik.
Welche ? Prädikatenlogik 2. Stufe ?



Eine Definition kann verständlich sein, auch wenn die für ihre nähere formale Analyse benötigte Mathematik nicht-trivial ist. Genau das ist hier der Fall: Zum Verständnis "benötigt" man nur die Konzepte "Zeichenkette", "Menge", "Regelanwendung", in der Folge kann man prüfen, ob eine Zeichenkette die Definition erfüllt.

Wenn man in einer Definition mathematische Konzepte benutzt, dann können die verschieden komplex bzw. formal sein:
- naive Liste (ohne weitere Präzisierung)
- Liste als spezielle Menge in der naiven Mengenlehre
- Liste als spezielle Menge in der axiomatischen Mengenlehre
Das Problem:
Wenn man sich aber in der Definition auf komplexe bzw. formale Begriffe zurückzieht (wie z.B. axiomatischen Mengenlehre AXM), dann benötigen diese formale Begriffe wieder eine Definition. Es kann sogar zirkulär werden:
Die Prädikatenlogik benötigt den Begriff der Menge.
Wählt man für Menge die  axiomatischen Mengenlehre, dann ist diese ja in FOL formalisiert.
Also FOL- AXM - FOL - AXM - ...
Also ein Zirkel.

Andererseits:
Wenn man sich in Definitionen auf Metaebene für die natürliche Sprache bzw. halbformale Begriffe bezieht (wie z.B. naive Menge, naive Liste, usw.), dann frage ich mich, warum überhaupt die die axiomatische Mengenlehre eingeführt wurde.
Man könnte doch mit der naiven Mengenlehre in der Metasprache und einer eingeschränkten Möglichkeit Mengen zu basteln auskommen ?
Was spricht dagegen ?


mfg
cx



  Profil  Quote  Link auf diesen Beitrag Link
smirk_mirkin
Junior Letzter Besuch: in der letzten Woche
Dabei seit: 04.12.2014
Mitteilungen: 17
Aus: Leipzig, Deutschland
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.17, eingetragen 2019-07-17


2019-07-17 10:23 - carlox in Beitrag No. 16 schreibt:
Hallo smirk_mirkin,
Gibt es ein reines Logikstudium oder ist das in ein anderes Studium eingebettet ?
Wo kann man das studieren ?
Gibt es dazu Infos (z.B. über die Vorlesungen) ?

Ja, das gibt es.

An der Uni Leipzig gibt es einen nicht-konsekutiven Master mit dem Titel "Logik und Wissenschaftstheorie". Leider wird der Studiengang langfristig keinen Bestand haben. Man kann Logik aber beispielsweise auch in München studieren.


Ich versuche mal konkret zu werden, weil ich sonst nicht weiss, ob wir noch von der gleichen Sache reden.

Fall1: Satz ist in FOL formulierbar
Beispiel: PA bedeuten die Peano-Axiome .
Man will z.B. zeigen, dass in allen Modellen gilt:
x=0 und y=0 ==> x+y=0
Man will also zeigen:
$PA \models x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow
x \oplus y \equiv \overline{0} $
Nach dem Vollständigkeitssatz genügt zu zeigen:
$PA \vdash x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow
x \oplus y \equiv \overline{0} $
Ok, jetzt ist man auf FOL-Ebene mit den FOL-Sclussregeln und kann dann einen Beweis in FOL machen.

Fall2: Satz ist nicht in FOL formulierbar
Beispiel:
$\quad \Sigma \vdash \varphi \implies \Sigma \models \varphi$
Den Beweis kann man jetzt nicht mehr auf FOL-Ebene machen.
man braucht eine Metalogik.
Welche ? Prädikatenlogik 2. Stufe ?

Fall3: Satz ist nicht in FOL formulierbar
Beispiel:
Alle ganzen, natürlichen Zahlen grösser 2 sind im Standardmodell als Summe zweier Primzahlen darstellbar.
Angenommen der Satz ist wahr.
Der Beweis ist nicht mehr auf FOL-Ebene machbar.
man braucht eine Metalogik.
Welche ? Prädikatenlogik 2. Stufe ?

Deine Ausführungen berühren unterschiedlichste Themen und sind unscharf, so dass es mir schwer fällt deine Gedanken nachzuvollziehen. Deswegen hole ich etwas aus.

Immer dann, wenn wir Mathematik treiben, benutzen wir die mathematische Metasprache, die auf eine Metalogik zurückgreift. IMMER. Die Logik ist schließlich die Game-Mechanik der Mathematik. Wenn du nun eine Aussage beweisen willst (egal ob über Logik oder was anderes), dann ist die zwar in der Metasprache formuliert, implizit willst du aber nachweisen, dass eine Formel in der Metalogik allgemeingültig ist.

Wie stellt man das an? Man benutzt Schlussregeln, also Regeln die allgemeingültige Aussagen in allgemeingültige Aussagen umwandeln. Dieses Vorgehen nennt man Beweisen.

Erkenntnisse über dieses Vorgehen erhalten wir, indem wir die Logik untersuchen. Oder auch nur ein Fragment davon, zum Beispiel FOL. Dafür benutzen wir aber natürlich auch wieder die Metalogik (die auch FOL enthält), also müssen wir hier von Anfang an zwei Ebenen unterscheiden: Die zu untersuchende Objektlogik und die zur Untersuchung benutzte Metalogik (eingebettet in Metasprache).

Also auch in deinem Beispiel 1 bist du die ganze Zeit auf der Metaebene. Die PA sind hier Elemente deiner Objektlogik, du redest ÜBER sie. Der Satz $PA \models x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow x \oplus y \equiv \overline{0} $ ist eine Aussage der Metalogik, wenn man so will also eine mit vielen Abkürzungen übersäte High-Level-Formel, deren Gültigkeit du nachweisen willst.

Was man mit welcher Logik wie formulieren kann ist ein ganz anderes Thema und nicht mal einfach so zu beantworten. Da kommt dann für die Mathematik noch die Mengenlehre ins Spiel.


Andererseits:
Wenn man sich in Definitionen auf Metaebene für die natürliche Sprache bzw. halbformale Begriffe bezieht (wie z.B. naive Menge, naive Liste, usw.), dann frage ich mich, warum überhaupt die die axiomatische Mengenlehre eingeführt wurde.
Man könnte doch mit der naiven Mengenlehre in der Metasprache und einer eingeschränkten Möglichkeit Mengen zu basteln auskommen ?
Was spricht dagegen ?

Wie du schon erkannt hast ist es unmöglich, alle Konzepte sauber aus dem Nichts zu definieren. Du brauchst immer ein Fundament und du musst immer irgendwo mathematische Intuition voraussetzen, zum Beispiel bei der Definition der Logik. Die axiomatische Methode ist der Versuch, dies zu minimieren (und liefert weitere Vorteile). Trotzdem brauchst du auch mit Axiomensystemen noch nicht-formale Einsichten oder Begriffe.

Bezüglich der naiven Mengenlehre: mit ihr kann man auskommen. Man führt sie schließlich im Studium ein und baut darauf. Nebenbei weist man darauf hin, dass naive Mengen gewisse Schwierigkeiten machen können.

Trotzdem möchte man natürlich wissen: "Was darf ich?", "Wo muss ich aufpassen?" und "Was geht eigentlich alles mit formalen Mitteln, ohne Probleme zu bekommen?" Also untersuchen Menschen die Mengenlehre und fanden dabei eine gewissermaßen gute Axiomatisierung des Mengenbegriffs.

Benutzt man heute in einer alltäglichen mathematischen Abhandlung den Begriff der Menge, so spezifiziert man meist nicht, ob man eine ZF-Menge meint oder ob man eine naive Menge meint. Denn wie schon geschrieben: In vielen Bereichen ist einem das fast egal.

Nachsatz

Ein sinnvoller Schritt hin zu mehr Klarheit ist das präzise Formulieren von Fragen und Gedanken. Denn bei der Suche nach einer klaren Formulierung kann sich so manches Problem schon erübrigen.

Du verwendest einige schwer verständliche Ausdrücke, z.B.:


[...] in Definitionen auf Metaebene für die natürliche Sprache [...]
Ich gehe nicht davon aus, dass du hier Sprache definieren möchtest.

[...] warum überhaupt die die axiomatische Mengenlehre eingeführt wurde.
Wie wurde die denn eingeführt? Sie wurde höchstens betrieben und Leute beziehen sich in einer, der näheren Erklärung bedürfender, Form darauf.



  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 190
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.18, eingetragen 2019-07-17


2019-07-17 10:23 - carlox in Beitrag No. 16 schreibt:

...Wenn wir nun Beweise führen, so tun wir das informell, beziehen uns dabei jedoch auf Schlussregeln unserer Metalogik. Welche diese Metalogik ist, ist hingegen nicht so leicht zu beantworten. In der Regel wird es Prädikatenlogik höherer Stufe sein.
Gut, dass ich jetzt auch nicht alleine bin (Zitat ZA:
"Weil man das nicht braucht. Ich habe es nie vermißt, und bin dabei offenbar nicht alleine.")
Hätte mich bei einem Logikstudium auch gewundert, dass man das ausblendet.

Bei Dir geht vieles durcheinander. In No. 9 schreibst Du 'Habe kein Problem, dass man "die informelle, in natürlicher Sprache formulierte, Mathematik letztendlich nie los wird". Angenommen, man formalisert einen metasprachlichen Beweis so weit wie möglich. Dann habe ich folgende Kritik: Warum werden die Regeln, Schlussweisen usw., die man in metasprachlichen Beweisen verwendet, _nirgends_ angegeben?'

Zuerst sprichst Du von informeller, natürlicher Sprache, und dann auf einmal von Metasprache. Nennen wir mal die natürliche, mit mathematischen Zeichen angereichte, Sprache einfach "informelle Sprache". Dann müßte Deine Frage lauten: Angenommen, man formalisert einen informel-sprachlichen Beweis so weit wie möglich. Dann habe ich folgende Kritik: Warum werden die Regeln, Schlussweisen usw., die man in informel-sprachlichen Beweisen verwendet, _nirgends_ angegeben?

Mit Metasprache hat das nichts zu tun. In Metasprache spricht man ÜBER die Objektsprache. Die Metasprache kann sowohl informell sein (so wie bei Ebbinghaus, wenn er die Semantik von FOL definiert) oder auch formal, so wie bei 'tactac' in seinem Lean-Beispiel aus No. 1.

Zu Deinem Anliegen mal ein Beispiel. Angenommen, man findet in einem Buch oder Artikel folgende Argumentation: Da p > 2 und Primzahl ist, gibt es ein n > 0 mit p = 2*n + 1. Folglich ...".

Jetzt sagst Du: Klar, das habe ich verstanden. Und das ist ohne Frage auch richtig. Aber wie belegt man das eigentlich? Es müßte doch ein informel-sprachliches Regelsystem geben, mit dem man aus "p > 2 und Primzahl" herleiten kann, daß "es gibt ein n > 0 mit p = 2*n + 1" gilt.

Und dazu habe ich geantwortet, daß es das nicht gibt, da man es nicht braucht. Entweder man bleibt auf der informellen Ebene, zu der eben auch die nirgends definierte Semantik der natürlichen Sprache gehört, oder man wechselt auf die formale Ebene. Ein informel-sprachliches Regelsystem ist weder formal noch informel, es wäre irgendein unbrauchbarer Mischmasch.



Den Beweis kann man jetzt nicht mehr auf FOL-Ebene machen.
man braucht eine Metalogik.
Welche ? Prädikatenlogik 2. Stufe ?

Was ist denn eine 'Metalogik', und warum braucht man die hier? Angenommen, wir wollen zeigen, daß in einer Gruppe das links-neutrale Element auch rechts-neutral ist. Wir beginnen mit Aussagenlogik und stellen fest, daß Aussagenlogik zu ausdrucksschwach ist, um unser Problem zu formulieren. Nehmen wir jetzt eine 'Metalogik'? Nein, wir wählen eine ausdrucksstärkere Logik, etwa FOL, und definieren darin die Gruppenaxiome und beweisen die Behauptung.

Anderes Beispiel: Es ist beweisbar, daß das Goodstein Theorem nicht in Peano-Arithmetik beweisbar ist. Was nun? Eine 'Metalogik'. Nein, man führt den Beweis dann in Logik 2. Stufe.

2019-07-17 14:52 - smirk_mirkin in Beitrag No. 17 schreibt:
Nachsatz

Ein sinnvoller Schritt hin zu mehr Klarheit ist das präzise Formulieren von Fragen und Gedanken. Denn bei der Suche nach einer klaren Formulierung kann sich so manches Problem schon erübrigen.

Das sehe auch auch so, und das fehlt Dir hier. Außerdem habe ich den Eindruck, daß Du über die Antworten auf Deine Fragen nicht weiter nachdenkst, sondern statt dessen versuchst Deinen Standpunkt zu "retten". Ein Beispiel dafür ist Deine Frage, warum man Deinen "intuitiven und einfachen" Vorschlag die Addition zu definieren nicht in Lehrbüchern findet. Ich gebe Dir dazu ein Beispiel aus dem ersichtlich wird, daß diese Definition eben nicht einfach ist, wenn man Beweise führen will. Aber darüber denkst Du nicht nach, sondern kommst mit dem "Gegenargument", daß man ohnehin die Äquivalenz beider Definitionen zeigen muß. Was soll das? Wenn man Deine Definition nicht verwendet weil sie ungeeignet ist für das Führen von Beweisen in der Arithmetik, dann erübrigt sich solch ein Beweis. Und wenn man die Äquivalenz beweist, um die Korrektheit der Schulmethode zu belegen, dann folgt doch daraus nicht, daß die Schulmethode "intuitiv und einfach" ist um Beweise in der Arithmetik zu führen.



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.19, vom Themenstarter, eingetragen 2019-07-18



Bei Dir geht vieles durcheinander….
Ja, ich bin schon etwas verwirrt und habe noch keine Klarheit über den Sachverhalt erlangt.    
Deswegen vielen  Dank für eure wertvollen Feedbacks.
Auch wird auf dieses Thema nicht im Mathematikstudium eingegangen.
Oder kennt jemand von euch dazu Quellen ?


Nennen wir mal die natürliche, mit mathematischen Zeichen angereichte, Sprache einfach "informelle Sprache".
Ok nehmen wir diesen  Begriff als gemeinsame Grundlage.


Dann müßte Deine Frage lauten: Angenommen, man formalisert einen informel-sprachlichen Beweis so weit wie möglich. Dann habe ich folgende Kritik: Warum werden die Regeln, Schlussweisen usw., die man in informel-sprachlichen Beweisen verwendet, _nirgends_ angegeben?
ok


Jetzt sagst Du: Klar, das habe ich verstanden. Und das ist ohne Frage auch richtig. Aber wie belegt man das eigentlich? Es müßte doch ein informel-sprachliches Regelsystem geben, mit dem man aus "p > 2 und Primzahl" herleiten kann, daß "es gibt ein n > 0 mit p = 2*n + 1" gilt.
Und dazu habe ich geantwortet, daß es das nicht gibt, da man es nicht braucht. Entweder man bleibt auf der informellen Ebene, zu der eben auch die nirgends definierte Semantik der natürlichen Sprache gehört, oder man wechselt auf die formale Ebene. Ein informel-sprachliches Regelsystem ist weder formal noch informel, es wäre irgendein unbrauchbarer Mischmasch.
Ich habe dich so verstanden:
Für einen informellen Beweis braucht man kein informelles, sprachliches Regelsystem, weil es ja  eine formale Ebene gibt. D.h. wem ein informeller Beweis nicht genügt, der kann ja einen formalen Beweis erstellen.
Habe ich dich damit richtig verstanden ?

Jetzt zum Begriff "Beweis"
Wenn man zu jedem Satz einen formalen Beweis liefern will, muss zuerst geklärt werden:
Was ist ein formaler Beweis und wo wird er definiert?
Mein Vorschlag:
Ein formaler Beweis ist eine endliche Folge, wobei jedes Folgenglied durch frühere Folgenglieder durch Anwendung einer Schlussregel entsteht oder ein Axiom ist.
Der Begriff "Beweissystem" (Ein Beweissystem ist ein Quadrupel ...) wird definiert (formalisiert) in Komplexitätstheorie von W.J. Paul Teubner Studienbücher Informatik. Hier ein Auzug (wichtigster Teil). Vermutlich meinst du das mit "Logik". Siehe:
drive.google.com/file/d/1TrdMWg5bWmQdjToxi9Cehh9KXNAqHF4V/view?usp=sharing

Frage:
In welchem Verhältnis steht ein Beweis und die Metasprache / Metalogik ?

Zitate smirk_mirkin (vielleicht kann er auch noch etwas dazu beitragen)
"Immer dann, wenn wir Mathematik treiben, benutzen wir die mathematische Metasprache, die auf eine Metalogik zurückgreift. IMMER."
"...Wenn wir nun Beweise führen, so tun wir das informell, beziehen uns dabei jedoch auf Schlussregeln unserer Metalogik."

In den folgenden Beispielen bitte ich euch die Logik (formale Ebene), anzugeben bzw. die Sprache anzugeben, in der die Sätze formuliert sind bzw. das komplette Beweissystem.
(Warum ist hier der Begriff Metalogik falsch bzw. was versteht  man darunter?)

Beispiel1:
Satz:
$PA \vdash x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow
x \oplus y \equiv \overline{0} $

Meiner Meinung nach ist hier FOL das Beweissystem.

Beispiel2:
Satz:
$PA \models x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow
x \oplus y \equiv \overline{0} $

Beweissystem: ?

Beispiel3:
Satz:
$\quad \Sigma \vdash \varphi \implies \Sigma \models \varphi$

Beweissystem: ?

Beispiel4:
Satz:
Alle ganzen, natürlichen Zahlen grösser 2 sind im Standardmodell von PA als Summe von höchstens 5 Primzahlen darstellbar.

Beweissystem: ?



... Außerdem habe ich den Eindruck, daß Du über die Antworten auf Deine Fragen nicht weiter nachdenkst, sondern statt dessen versuchst Deinen Standpunkt zu "retten". Ein Beispiel dafür ist Deine Frage, warum man Deinen "intuitiven und einfachen" Vorschlag die Addition zu definieren nicht in Lehrbüchern findet. Ich gebe Dir dazu ein Beispiel aus dem ersichtlich wird, daß diese Definition eben nicht einfach ist, wenn man Beweise führen will. Aber darüber denkst Du nicht nach, ....
Ich war mit deinen Ausführungen einverstanden, habe dies aber nicht explizit formuliert.


... Und wenn man die Äquivalenz beweist, um die Korrektheit der Schulmethode zu belegen, dann folgt doch daraus nicht, daß die Schulmethode "intuitiv und einfach" ist um Beweise in der Arithmetik zu führen.
ja

mfg
cx



  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 02.12.2013
Mitteilungen: 190
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.20, eingetragen 2019-07-18


2019-07-18 15:07 - carlox in Beitrag No. 19 schreibt:
Ich habe dich so verstanden:
Für einen informellen Beweis braucht man kein informelles, sprachliches Regelsystem, weil es ja  eine formale Ebene gibt. D.h. wem ein informeller Beweis nicht genügt, der kann ja einen formalen Beweis erstellen.
Habe ich dich damit richtig verstanden ?

Im Prinzip ja. Die Maxime wäre, daß jeder informelle Beweis formal nachvollziehbar sein muß. Das ist natürlich eine sehr starke Forderung. De facto passiert Folgendes: Wenn ein Gutachter einer Fachzeitschrift eine Folgerung im (informellen) Beweis einer eingereichten Arbeit nicht versteht, dann bittet er den Autor seine Schlußweise zu präzisieren, also Lücken zu schließen. Informelle Beweise werden ja dadurch erst kommunizierbar, daß "offensichtliches" weggelassen und auf das Vorwissen und die Expertise des Lesers vertraut wird. So kann man bei Bedarf einen Beweis immer weiter detailieren, bis wirklich alles offensichtlich ist.

Beispiel: Andrew Wiles hatte den ersten Entwurf seines Beweises des "Großen Fermat" an eine handvoll von Experten zur Durchsicht gegeben. Einer davon konnte eine Folgerung nicht nachvollziehen und bat um Klärung. Zunächst sah das wie eine Routinesache aus, doch es stellte sich dann heraus, daß die "Lücke" gravierend war. Es hat dann einige Zeit und Arbeit gekostet, die Lücke zu schließen. So funktioniert das in der Praxis (wobei manche Lücken nie geschlossen werden, weil die Behauptung nicht beweisbar ist, und auch nicht-schließbare Lücken übersehen werden).    


Frage:
In welchem Verhältnis steht ein Beweis und die Metasprache / Metalogik ?

Ich kann dazu nichts sagen, da ich den Begriff "Metalogik" nicht verwendet habe.


In den folgenden Beispielen bitte ich euch die Logik (formale Ebene), anzugeben bzw. die Sprache anzugeben, in der die Sätze formuliert sind bzw. das komplette Beweissystem.
(Warum ist hier der Begriff Metalogik falsch bzw. was versteht  man darunter?)

Beispiel1:
Satz:
$PA \vdash x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow
x \oplus y \equiv \overline{0} $

Meiner Meinung nach ist hier FOL das Beweissystem.

Beispiel2:
Satz:
$PA \models x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow
x \oplus y \equiv \overline{0} $

Beweissystem: ?

Beispiel3:
Satz:
$\quad \Sigma \vdash \varphi \implies \Sigma \models \varphi$

Beweissystem: ?

Beispiel4:
Satz:
Alle ganzen, natürlichen Zahlen grösser 2 sind im Standardmodell von PA als Summe von höchstens 5 Primzahlen darstellbar.

Beweissystem: ?

Was bezweckst Du mit diesen Fragen, welche Erkenntnisse denkst Du daraus zu gewinnen?

Man wird kein Pilot indem man nur Bücher über das Fliegen liest. Du solltest mal etwas Erfahrung sammeln, und Erfahrung gewinnt man nur indem man die Ärmel hochkrempelt und die Sachen konkret anpackt. Der Beweis der Gleichheit beider Definitionen der Addition wäre ein gutes Einsteigerbeispiel.

 



  Profil  Quote  Link auf diesen Beitrag Link
smirk_mirkin
Junior Letzter Besuch: in der letzten Woche
Dabei seit: 04.12.2014
Mitteilungen: 17
Aus: Leipzig, Deutschland
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.21, eingetragen 2019-07-18


(2019-07-18 15:07 - carlox in <a href=viewtopic.php?topic=242584&
Ja, ich bin schon etwas verwirrt und habe noch keine Klarheit über den Sachverhalt erlangt.    
Du wirst durch diesen einen Thread auch keine Klarheit erlangen.
Lies am besten noch einmal aufmerksam, was wir geschrieben haben bzw. schreiben und dann arbeite mal wirklich die ersten 5 Kapitel von Ebbinghaus durch. Dann wirst du zwar noch immer keine Klarheit haben, aber gewisse Missverständnisse werden sich auflösen.


Ich habe dich so verstanden:
Für einen informellen Beweis braucht man kein informelles, sprachliches Regelsystem, weil es ja  eine formale Ebene gibt. D.h. wem ein informeller Beweis nicht genügt, der kann ja einen formalen Beweis erstellen.
Habe ich dich damit richtig verstanden ?
Ja.


Jetzt zum Begriff "Beweis"
[...]
Frage:
In welchem Verhältnis steht ein Beweis und die Metasprache / Metalogik ?
Mathematische Aussagen sind formal betrachtet Formeln einer Logik. Diese bezeichne ich gelegentlich als Metalogik, da sie uns auch bei informellen mathematischen Abhandlungen aus dem Hintergrund heraus leitet.

Beweisen ist der Nachweis einer Folgerungsbeziehung zwischen einer Axiomenmenge und der zu beweisenden Aussage. Dieser Nachweis kann formal im Rahmen eines Kalküls ("Beweissystem")  erbracht werden. Ein Kalkül ist in diesem Kontext ein System von (Schluss-)Regeln, das Formeln in andere Formeln umwandelt und dabei die Folgerungsbeziehung erhält. Ein Beweis ist eine endliche Folge solcher Regelanwendungen.

Es gibt viele verschiedene Kalküle für FOL.


In den folgenden Beispielen bitte ich euch die Logik (formale Ebene), anzugeben bzw. die Sprache anzugeben, in der die Sätze formuliert sind bzw. das komplette Beweissystem.
(Warum ist hier der Begriff Metalogik falsch bzw. was versteht  man darunter?)

Also erstens habe ich ja schon gesagt, dass es gar nicht so klar ist, was die Metalogik eigentlich ist. Denn einfache Prädikatenlogik erster Stufe reicht schon nicht mal mehr, um Erreichbarkeit in einfachen Relationen auszudrücken. Deswegen braucht man noch Mengenlehre dazu oder eben Logik höherer Stufe ... Keine Ahnung. Und wie gesagt, es gibt dann zusätzlich sogar noch verschiedene "Beweissysteme", die man benutzen kann.

Zweitens ist das viel zu viel Arbeit.

Gehässiger Vorschlag: Schau dir die Principa Mathematica an, da wird die Arithmetik komplett formal erarbeitet.

Ernst gemeiner Vorschlag: Nimm dir den Ebbinghaus, schau dir den Sequenzenkalkül an. Nimm dir einfachere Aussagen und dann probier es aus, die formal zu beweisen.


Beispiel1:
Satz:
$PA \vdash x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow
x \oplus y \equiv \overline{0} $

Meiner Meinung nach ist hier FOL das Beweissystem.

FOL ist kein Beweissystem, sondern die Logik auf der ein Beweissystem aufsetzt. Und noch mal (wie mehrfach oben geschrieben): Du verwirrst dich hier selber, weil du Aussagen ÜBER Logik IN Logik formalisieren willst, was für dein Verständnis erstmal vollkommen unnötig ist.

WICHTIG: Es macht einen (formalen) Unterschied, ob man in einem Kalkül vor dem Hintergrund der Peano-Axiome die Formel $x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow x \oplus y \equiv \overline{0}$ beweisen will oder ob man die Aussage $PA \vdash x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow x \oplus y \equiv \overline{0}$ über einen best. Kalkül auf Metaebene beweisen will.

Im ersten Fall gibt man im zu betrachtenden Kalkül einen formalen Beweis der Form $PA \vdash Formel$ an. Im zweiten Fall müsste man die gesamte Aussage erst einmal in eine "elementare" Formel überführen, also vor allem alle "Abkürzungen" aufdröseln. Ich mach das aus pragmatischen Gründen kurz am Beispiel 2 vor:

$PA \models x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow
x \oplus y \equiv \overline{0}$ wird zu
$\models\big(\ \{ \dots\text{Peano-Axiome}\dots \},\ x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow x \oplus y \equiv \overline{0}\ \big)$ wird zu
$\forall\mathcal{I}.\Big( \text{istInterprVon}\big(\mathcal{I}, \{ \dots\text{Peano-Axiome}\dots \}\big) \implies \text{istInterprVon}\big(x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow x \oplus y \equiv \overline{0} \big)\Big)$
und so weiter ...

Das Prinzip sollte klar sein. Irgendwann hast du eine metalogische Riesenformel $\varphi$ mit Mengenausdrücken. Dann nimmst du dir einen FO-Kalkül $K$ und beweist $ZF \vdash_K \varphi$.

Zwischen Beispiel 1 und 2 sehe ich keinen prinzipiellen Unterschied. Außer dem, dass überhaupt nicht klar ist, was $\vdash$ für dich bedeutet. Mach dir das bitte noch mal klar.



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.22, vom Themenstarter, eingetragen 2019-07-18



Was bezweckst Du mit diesen Fragen, welche Erkenntnisse denkst Du daraus zu gewinnen?

Damit kann ich feststellen, ob meine Überlegungen korrekt sind.

mfg
cx



  Profil  Quote  Link auf diesen Beitrag Link
smirk_mirkin
Junior Letzter Besuch: in der letzten Woche
Dabei seit: 04.12.2014
Mitteilungen: 17
Aus: Leipzig, Deutschland
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.23, eingetragen 2019-07-19


Ich habe meine vorherige Antwort gerade etwas überarbeitet, da mir Fehler und Ungenauigkeiten aufgefallen sind!



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.24, vom Themenstarter, eingetragen 2019-07-20


Hallo smirk_mirkin,
danke für dein feedback.


FOL ist kein Beweissystem, sondern die Logik auf der ein Beweissystem aufsetzt.
Schau mal den Link auf Paul (in einer früheren email von mir) an.
Da ist FOL schon ein Beweissystem: Alphabet, Sprache, Axiome, Schlussregeln


WICHTIG: Es macht einen (formalen) Unterschied, ob man in einem Kalkül vor dem Hintergrund der Peano-Axiome die Formel $x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow x \oplus y \equiv \overline{0}$ beweisen will
ja, so etwas habe ich schon zur Genüge getan


oder ob man die Aussage $PA \vdash x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow x \oplus y \equiv \overline{0}$ über einen best. Kalkül auf Metaebene beweisen will.
genau.


Im ersten Fall gibt man im zu betrachtenden Kalkül einen formalen Beweis der Form $PA \vdash Formel$ an.
genau.


Im zweiten Fall müsste man die gesamte Aussage erst einmal in eine "elementare" Formel überführen, also vor allem alle "Abkürzungen" aufdröseln.
ja


Ich mach das aus pragmatischen Gründen kurz am Beispiel 2 vor:
$PA \models x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow
x \oplus y \equiv \overline{0}$ wird zu
$\models\big(\ \{ \dots\text{Peano-Axiome}\dots \},\ x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow x \oplus y \equiv \overline{0}\ \big)$ wird zu
$\forall\mathcal{I}.\Big( \text{istInterprVon}\big(\mathcal{I}, \{ \dots\text{Peano-Axiome}\dots \}\big) \implies \text{istInterprVon}\big(x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow x \oplus y \equiv \overline{0} \big)\Big)$
und so weiter ...
Ich habs auch mal probiert (Ebbinghaus):
$PA \models x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow  x \oplus y \equiv \overline{0} $
gdw
für alle Modelle  $(\mathfrak{A},h)$  wenn ($\mathfrak{A},h) \models PA$ dann $(\mathfrak{A},h) \models
x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow  x \oplus y \equiv \overline{0} $
gdw
für alle Modelle  $(\mathfrak{A},h)$  wenn ($\mathfrak{A},h) \models PA$ dann
$(\mathfrak{A},h) \models
x \equiv \overline{0} \land y \equiv \overline{0} \Longrightarrow (\mathfrak{A},h) \models x \oplus y \equiv \overline{0} $
gdw
für alle Modelle  $(\mathfrak{A},h)$  wenn ($\mathfrak{A},h) \models PA$ dann h(x)=$0^\mathfrak{A}$ und h(y)=$0^\mathfrak{A}$ $\Longrightarrow$ h(x) $+^\mathfrak{A}$ h(y)=$0^\mathfrak{A}$
Jetzt muss man noch $\models$ auflösen (wegbekommen analog zu obigen Auflösungen).
Dann habe ich noch "wenn dann" bzw "und" als "natürlichsprachliche Junktoren" (ist das der richtige Ausdruck ?)
Diese "natürlichsprachlichen Junktoren" sind natürlichsprachlich formuliert (siehe Ebbinghaus).
"wenn dann" habe ich teilweise schon ersetzt durch: $\Longrightarrow$
(als Abkürzung für das lange "wenn dann").
So, jetzt hat man also ein Mischmasch aus "natürlichsprachlichen Junktoren", Mengen und Funktionen.
Das wird jetzt alles in FOL formalisiert:
Aus der Funktion $+^\mathfrak{A}$ und $0^\mathfrak{A}$ wird jeweils eine Menge und aus "wenn dann" wird $\rightarrow$ bzw. aus
"und" wird $\land$
Hast du das gemeint ?


Das Prinzip sollte klar sein. Irgendwann hast du eine metalogische Riesenformel $\varphi$ mit Mengenausdrücken. Dann nimmst du dir einen FO-Kalkül $K$ und beweist $ZF \vdash_K \varphi$.
ja


Zwischen Beispiel 1 und 2 sehe ich keinen prinzipiellen Unterschied. Außer dem, dass überhaupt nicht klar ist, was $\vdash$ für dich bedeutet. Mach dir das bitte noch mal klar.
$\vdash$ ist das Zeichen für Beweisbarkeit in FOL, oder auf was willst du hinaus?

Frage:
\(\)Man hat also die Semantik übersetzt in Beweisbarkeit in FOL bzgl. ZF
Könnte man dann nicht prinzipiell auf die Definition von Semantik verzichten und gleich dies auf Beweisbarkeit reduzieren ?

mfg
cx






  Profil  Quote  Link auf diesen Beitrag Link
smirk_mirkin
Junior Letzter Besuch: in der letzten Woche
Dabei seit: 04.12.2014
Mitteilungen: 17
Aus: Leipzig, Deutschland
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.25, eingetragen 2019-07-21 13:59


(2019-07-20 09:45 - carlox in <a href=viewtopic.php?topic=242584&
Dann habe ich noch "wenn dann" bzw "und" als "natürlichsprachliche Junktoren" (ist das der richtige Ausdruck ?)
Diese "natürlichsprachlichen Junktoren" sind natürlichsprachlich formuliert (siehe Ebbinghaus).

Ja, die sind natürlichsprachig formuliert, aber lassen sich auffassen als die Junktoren der Metalogik.


"wenn dann" habe ich teilweise schon ersetzt durch: $\Longrightarrow$
(als Abkürzung für das lange "wenn dann").
So, jetzt hat man also ein Mischmasch aus "natürlichsprachlichen Junktoren", Mengen und Funktionen.
Das wird jetzt alles in FOL formalisiert:
Aus der Funktion $+^\mathfrak{A}$ und $0^\mathfrak{A}$ wird jeweils eine Menge und aus "wenn dann" wird $\rightarrow$ bzw. aus
"und" wird $\land$
Hast du das gemeint ?

Ja genau das habe ich gemeint.

Abbildungen sind nur spezielle Mengen. Und ob man das jetzt "noch" formalisieren muss, ist letztlich eine unwichtige Nebenfrage. Es ist ja auch mit natürlichsprachlichen Junktoren offensichtlich, dass in gewissem Sinne eine Formel vorliegt, denn wie die Junktoren einer Logik aussehen ist schlicht egal.


$\vdash$ ist das Zeichen für Beweisbarkeit in FOL, oder auf was willst du hinaus?

Ich will darauf hinaus, dass Beweisbarkeit kein klarer Begriff ist, denn er sollte sich immer auf einen konkreten Kalkül beziehen. Ohne diese Angabe kann man eigentlich nicht wissen, was die Aussage bedeutet.

Aus dem gleichen Grund (und noch anderen) ist FOL kein guter Name für einen Kalkül.


Frage:
\(\)Man hat also die Semantik übersetzt in Beweisbarkeit in FOL bzgl. ZF
Könnte man dann nicht prinzipiell auf die Definition von Semantik verzichten und gleich dies auf Beweisbarkeit reduzieren ?

Nein, wir haben jetzt gezeigt, dass man die Aussage aus dem Beispiel als eine mit Mengenausdrücken angereicherte FO-Formel auffassen kann. Für diese Art von Logik gibt es keinen adäquaten Kalkül, also stimmen Beweisbarkeit und Gültigkeit hier nicht überein. Und warum sollte man auch überhaupt Semantik über Beweisbarkeit definieren?

Zusätzlich haben wir gesehen, dass schon diese eine "Reduktion" komplexitätsmäßig quasi unausführbar ist und uns auch keinen Mehrwert bringt.

Ich wiederhole mich: Dieses System von Definitionen und der Verzicht auf vollformale Beweise macht die Mathematik erst möglich.



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.26, vom Themenstarter, eingetragen 2019-07-21 15:20


Hallo smirk_mirkin,

Ich will darauf hinaus, dass Beweisbarkeit kein klarer Begriff ist, denn er sollte sich immer auf einen konkreten Kalkül beziehen. Ohne diese Angabe kann man eigentlich nicht wissen, was die Aussage bedeutet.
Aus dem gleichen Grund (und noch anderen) ist FOL kein guter Name für einen Kalkül.

Wären dann ZF (in FOL formalisiert) oder PA (in FOL formalisiert) Namen für Kalküle?
Meinst du das ?


Frage:
Man hat also die Semantik übersetzt in Beweisbarkeit in FOL bzgl. ZF
Könnte man dann nicht prinzipiell auf die Definition von Semantik verzichten und gleich dies auf Beweisbarkeit reduzieren ?


Nein, wir haben jetzt gezeigt, dass man die Aussage aus dem Beispiel als eine mit Mengenausdrücken angereicherte FO-Formel auffassen kann.

... wobei es für diese Formel - ich nenne sie $\varphi$ - einen Beweis im Beweissystem (Kalkül) ZF gibt:
ZFC $\vdash \varphi$
Damit habe ich doch die Semantik übersetzt in Beweisbarkeit im Beweissystem (Kalkül) ZF.
Oder wo ist da mein Denkfehler?


Für diese Art von Logik gibt es keinen adäquaten Kalkül,
Doch: ZF
(zumindest habe ich dies im Buch Mengenlehre von Ebbinghaus so verstanden).


also stimmen Beweisbarkeit und Gültigkeit hier nicht überein. Und warum sollte man auch überhaupt Semantik über Beweisbarkeit definieren?
siehe oben


Zusätzlich haben wir gesehen, dass schon diese eine "Reduktion" komplexitätsmäßig quasi unausführbar ist und uns auch keinen Mehrwert bringt.
Ich wiederhole mich: Dieses System von Definitionen und der Verzicht auf vollformale Beweise macht die Mathematik erst möglich.
Das bestreite ich überhaupt nicht!
Ich will nur wissen, ob das theoretisch möglich ist bzw. ob meine Überlegungen korrekt sind.
Das ist ähnlich dem Zusammenhang zwischen einer Programmiersprache und dem zugehörigen Maschinencode.
Man arbeitet in der Hochsprache und der Maschinencode ist (für die meisten Programmierer) uninteressant.

mfg
cx




  Profil  Quote  Link auf diesen Beitrag Link
smirk_mirkin
Junior Letzter Besuch: in der letzten Woche
Dabei seit: 04.12.2014
Mitteilungen: 17
Aus: Leipzig, Deutschland
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.27, eingetragen 2019-07-21 16:55


ZF und PA sind zunächst keine Kalküle, sondern Axiommengen. Konsistente Kalküle für die Arithmetik sind unvollständig, also kann man gerade NICHT alle gültigen Aussagen über ZF beweisen.

Die Reduktion oben hat uns eine Formel in der Sprache von ZF geliefert, mehr nicht. Da ist noch kein Beweis passiert. Von daher weiß ich auch nicht, was du mit


Damit habe ich doch die Semantik übersetzt in Beweisbarkeit im Beweissystem (Kalkül) ZF.

meinst. Was heißt hier überhaupt Semantik? Warum ist irgendwas durch unser halbherzig durchgegangenes Beispiel gezeigt?

Du kannst mathematische Aussagen, auch aus der mathematischen Logik, in der Regel als mit Mengenausdrücken angereicherte Formeln auffassen. Aber das habe ich ja schon gefühlt 1000 mal gesagt.

Mit Mengenlehre habe ich mich aber auch noch nicht beschäftigt und bin dementsprechend vorsichtig mit irgendwelchen Meta-Beobachtungen.



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.28, vom Themenstarter, eingetragen 2019-07-23 19:52




meinst. Was heißt hier überhaupt Semantik? Warum ist irgendwas durch unser halbherzig durchgegangenes Beispiel gezeigt?
Mit Semantik meinte ich das: (siehe Ebbinghaus)
$PA \models x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow  x \oplus y \equiv \overline{0} $
wobei ich diese Formel mit $\varphi$ abkürze.

Jetzt kann man zeigen:
$PA \models x \equiv \overline{0} \land y \equiv \overline{0} \rightarrow  x \oplus y \equiv \overline{0} $
gdw
für alle Modelle  $(\mathfrak{A},h)$  wenn ($\mathfrak{A},h) \models PA$ dann h(x)=$0^\mathfrak{A}$ und h(y)=$0^\mathfrak{A}$ $\Longrightarrow$ h(x) $+^\mathfrak{A}$ h(y)=$0^\mathfrak{A}$
Jetzt muss man noch $\models$ auflösen (wegbekommen analog zu obigen Auflösungen).
Dann habe ich noch "wenn dann" bzw "und" als "natürlichsprachliche Junktoren"
Und das kann man im Beweissystem (Kalkül) ZF_E = Beweisssytem mit Axiomensystem ZF im Buch Mengenlehre von Ebbinghaus in FOL formalisieren.

D.h.
Um $PA \models \varphi$ zu zeigen genügt zu zeigen:
$ZF_E \vdash \varphi$
Warum geht das nicht ?


Du kannst mathematische Aussagen, auch aus der mathematischen Logik, in der Regel als mit Mengenausdrücken angereicherte Formeln auffassen.
Das habe ich oben doch gemacht, oder ?

mfg
cx





  Profil  Quote  Link auf diesen Beitrag Link
smirk_mirkin
Junior Letzter Besuch: in der letzten Woche
Dabei seit: 04.12.2014
Mitteilungen: 17
Aus: Leipzig, Deutschland
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.29, eingetragen 2019-07-31 15:32


Was sind denn die Schlussregeln von $ZF_E$?



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.30, vom Themenstarter, eingetragen 2019-07-31 16:40


2019-07-31 15:32 - smirk_mirkin in Beitrag No. 29 schreibt:
Was sind denn die Schlussregeln von $ZF_E$?
Komme gerade schlecht ins Internet.
Antworte Ende/ Anfang diese / nächstre Woche.

mfg
cx




  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 962
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.31, vom Themenstarter, eingetragen 2019-08-04 11:10


2019-07-31 15:32 - smirk_mirkin in Beitrag No. 29 schreibt:
Was sind denn die Schlussregeln von $ZF_E$?

Ebbinghaus schreibt in seinem Buch "Einführung in die Mengenlehre" auf S. 17:
"Die Ausdrücke der mengentheoretischen Sprache - wir nennen sie fortan einfach Ausdrücke - bilden eine Sprache der ersten Stufe.
Informationen über solche Sprachen findet man etwa in [Ebbinghaus, Thomas, Flum]"

Mit [Ebbinghaus, Thomas, Flum] ist das Buch
"Einführung in die mathematische Logik"
gemeint. Dort wird ein Sequenzenkalkül benutzt.

mfg
cx




  Profil  Quote  Link auf diesen Beitrag Link
carlox hat die Antworten auf ihre/seine Frage gesehen.
carlox wird per Mail über neue Antworten informiert.
Neues Thema [Neues Thema] Antworten [Antworten]    Druckversion [Druckversion]

 


Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2019 by Matroids Matheplanet
This web site was made with PHP-Nuke, a web portal system written in PHP. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]