NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
From MaRDI portal
Publication:5001547
DOI10.1017/S175502031900056XOpenAlexW2982918323WikidataQ126786033 ScholiaQ126786033MaRDI QIDQ5001547
Patrick M. Walsh, Wilfried Sieg
Publication date: 22 July 2021
Published in: The Review of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s175502031900056x
natural deductionproof analysishuman-oriented theorem provingreasoning with gapsverification in set theory
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
MATHEMATICAL RIGOR AND PROOF ⋮ The Cantor–Bernstein theorem: how many proofs? ⋮ Human-centered automated proof search
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proofs of the Cantor-Bernstein theorem. A mathematical excursion
- How to write a 21\(^{\text{st}}\) century proof
- On the relations between Georg Cantor and Richard Dedekind
- Set theory for verification. I: From foundations to functions
- Normal natural deduction proofs (in classical logic)
- Automated search for Gödel's proofs
- On the rules of suppositions in formal logic
- Set theory for verification. II: Induction and recursion
- A fully automatic theorem prover with human-style output
- An automated prover for Zermelo-Fraenkel set theory in Theorema
- A lattice-theoretical fixpoint theorem and its applications
- A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
- Sir Timothy Gowers Interview
- David Hilbert's Lectures on the Foundations of Arithmetic and Logic 1917-1933
- Hilbert's Twenty-Fourth Problem
- MATHEMATICAL INFERENCE AND LOGICAL INFERENCE
- Dedekind's Abstract Concepts: Models and Mappings
- How to Write a Proof
- Computational Logic and Set Theory
- The Cantor–Bernstein theorem: how many proofs?
- A fixedpoint approach to implementing (Co)inductive definitions
- Mathematical Rigor, Proof Gap and the Validity of Mathematical Inference
- The challenge of computer mathematics
- Types for Proofs and Programs
- Zermelo and Set Theory
- Mechanizing Mathematical Reasoning
- On Computable Numbers, with an Application to the Entscheidungsproblem
- Practical forms of type theory
- Methodological Frames: Paul Bernays, Mathematical Structuralism, and Proof Theory
This page was built for publication: NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
