PhilSci Archive

On the formal justification of informal proofs

Bacelar Valente, Mario (2020) On the formal justification of informal proofs. [Preprint]

This is the latest version of this item.

[img]
Preview
Text
On the formal justification of informal proofs .pdf

Download (300kB) | Preview

Abstract

When modeling the informal proofs of Euclid’s Elements using the sound logical system E, we go from proofs seen as somewhat nonrigorous – even having gaps to be filled – to rigorous proofs. According to the ‘standard view’, the correctness of an informal proof is underwritten by the existence of a corresponding formal derivation. However, metalogic grounds the soundness of the logical system E, and proofs in metalogic are not like formal proofs and look suspiciously like informal proofs. In our view, they are informal proofs. This brings about what we are calling here the groundedness problem: how can we show with certainty that our metalogical proofs are correct and sustain our logical system? According to the ‘standard view’, we cannot. In this way, we would have to doubt the soundness of the formal system E. This in turn might lead us to doubt the justification of Euclidean informal proofs in terms of the corresponding formal proofs in E.


Export/Citation: EndNote | BibTeX | Dublin Core | ASCII/Text Citation (Chicago) | HTML Citation | OpenURL
Social Networking:
Share |

Item Type: Preprint
Creators:
CreatorsEmailORCID
Bacelar Valente, Mario
Keywords: Euclidean proof; metalogic; formal proof; informal proof; mathematical proof; metatheorems
Subjects: Specific Sciences > Mathematics > Logic
Specific Sciences > Mathematics > Proof
Specific Sciences > Mathematics
Depositing User: mario bacelar valente
Date Deposited: 12 May 2021 16:38
Last Modified: 12 May 2021 16:38
Item ID: 19031
Subjects: Specific Sciences > Mathematics > Logic
Specific Sciences > Mathematics > Proof
Specific Sciences > Mathematics
Date: 2020
URI: https://philsci-archive.pitt.edu/id/eprint/19031

Available Versions of this Item

Monthly Views for the past 3 years

Monthly Downloads for the past 3 years

Plum Analytics

Actions (login required)

View Item View Item