Reconsidering pairs and functions as sets

DOI10.1007/S10817-015-9340-6MaRDI QIDQ286796zbMATH OpenOpenAlexFDO

Authors Chad E. Brown

Publication date 26 May 2016

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-015-9340-6

zbMATH Keywords

functionshigher-order logichigher-order theorem provingordered pairsset theorysimple type theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Other classical set theory (including functions, relations, and set algebra) (03E20) Axiomatics of classical set theory and its fragments (03E30)

Recommendations

• Rethinking set theory
• Separating sets by functions and by sets
• EXTENDING SET FUNCTIONS AND RELATIONS
• Set functions and Souslin’s hypothesis
• scientific article; zbMATH DE number 1064005
• scientific article; zbMATH DE number 2118068
• scientific article; zbMATH DE number 3972859
• A note on separating function sets

Cites work

• Completeness and Cut-elimination in the Intuitionistic Theory of Types
• scientific article; zbMATH DE number 2185680 (Why is no real title available?)
• scientific article; zbMATH DE number 3427309 (Why is no real title available?)
• scientific article; zbMATH DE number 1420782 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3286022 (Why is no real title available?)
• scientific article; zbMATH DE number 3291106 (Why is no real title available?)
• scientific article; zbMATH DE number 3424017 (Why is no real title available?)
• Partizan Games in Isabelle/HOLZF
• Set theory for verification. I: From foundations to functions

Cited in

(11)

• A set theory with support for partial functions
• Adding an abstraction barrier to ZF set theory
• Encoding functional relations in Scunak
• On Pairs and Tuples
• Implementing mathematical objects in set theory
• Reconsidering Ordered Pairs
• Letter
• Two accounts of pairs
• Hammering higher order set theory
• Unordered pairs in the set theory of Bourbaki 1949
• Pairs, sets and sequences in first-order theories

Describes a project that uses

Uses Software

• Coq
• Isabelle/ZF

This page was built for publication: Reconsidering pairs and functions as sets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q286796)