Fitch notation

Fitch-notation , även känd som Fitch-diagram (uppkallat efter Frederic Fitch ), är ett notationssystem för att konstruera formella bevis som används i meningslogik och predikatlogik . Fitch-liknande bevis ordnar sekvensen av meningar som utgör beviset i rader. En unik egenskap hos Fitch-notation är att graden av indrag för varje rad visar vilka antaganden som är aktiva för det steget.

Exempel

Varje rad i ett Fitch-prov är antingen:

ett antagande eller underbevisande antagande.
en mening motiverad av citeringen av (1) en slutledningsregel och (2) den eller de föregående raderna i beviset som licenserar den regeln.

Införandet av ett nytt antagande ökar indragningsnivån och startar en ny vertikal "omfattnings"-stapel som fortsätter att dra in efterföljande rader tills antagandet uppfylls. Den här mekanismen förmedlar omedelbart vilka antaganden som är aktiva för en given rad i beviset, utan att antagandena behöver skrivas om på varje rad (som med sekventiska bevis).

Följande exempel visar huvuddragen i Fitch-notation:

0 |__ [antagande, vill P iff inte inte P] 1 | |__ P [antagande, vill inte inte P] 2 | | |__ inte P [antagande, för reduktion] 3 | | | motsägelse [motsägelseinledning: 1, 2] 4 | | inte inte P [negationsintroduktion: 2] | 5 | |__ inte inte P [antagande, vill ha P] 6 | | P [negeringseliminering: 5] | 7 | P iff inte inte P [bivillkorlig introduktion: 1 - 4, 5 - 6]

0. Nollantagandet, dvs. vi bevisar en tautologi 1. Vårt första underbevis: vi antar att lhs för att visa rhs följer 2. Ett undersubbevis: vi är fria att anta vad vi vill. Här siktar vi på en reductio ad absurdum 3. Vi har nu en motsägelse 4. Vi får prefixa påståendet som "orsakade" motsägelsen med en inte 5. Vårt andra underbevis: vi antar att rhs visar lhs följer 6. Vi åberopar regeln som tillåter oss att ta bort ett jämnt antal noter från ett satsprefix 7. Från 1 till 4 har vi visat om P då inte inte P, från 5 till 6 har vi visat P om inte P; därför får vi införa det bivillkorliga

Se även

Naturligt avdrag

Frederic Brenton Fitch , Symbolic Logic: An introduction , Ronald Press Co., 1952.
Jon Barwise och John Etchemendy , Language, Proof and Logic, första upplagan som PDF , Seven Bridges Press och CSLI, 1999.

externa länkar