SSL top_choice_facts.pvs
Interaktion und PortierbarkeitPVS
top_choice_facts: THEORY %------------------------------------------------------------------------------ % % Theories and proofs: relational and functional choice facts % based on Axiom of Choice % % Author: Dragan Stosic % % Short description: % % Axiom of Choice, represent a statement in the language of set theory % that makes it possible to form sets by choosing an element % simultaneously from each member of an infinite collection of sets even % when no algorithm exists for the selection. The axiom of choice has % many mathematically equivalent formulations, some of which were not % immediately realized to be equivalent. % % In this work I investigate the relations between the following choice % and description principles: % % rel_choice - Relational form of the (non extensional) axiom of choice % (a "set-theoretic" axiom of choice). Relational choice can be used to % extract from a relation a sub-relation that describes a function, by % mapping every argument to a unique image. % % fun_choice - Functional form of the (non extensional) axiom of choice % (a "type-theoretic" axiom of choice). This result can be used to % build a function from a relation that maps every input to at least one % output. % % rel_unique_choice - Unique relational form of the (non extensional) % axiom of choice (a "set-theoretic" axiom of choice) % % conditional_relational_choice - Conditional relational form of the % (non extensional) axiom of choice. % % parametric_definite_description - Functional Relation Reification % (known as Axiom of Unique Choice in topos theory; also called % principle of definite description. % % proof_irrelevance - as an identification treatment of all proofs of % the same proposition such that all proofs of the same proposition are % equal. % % Motivation and goal: % % In the PVS verification system ( based on classical logic ) I showed % that the functional formulation of the Axiom of Choice (usual % formulation in type theory) is equivalent to its relational % formulation (only formulation of set theory) plus parametric definite % description (aka Axiom of Unique Choice, or, Functional Relation % Reification ). This shows that the axiom of choice can be assumed % (under its relational formulation) without known inconsistency with % classical logic, though parametric definite description conflicts with % classical logic. %------------------------------------------------------------------------------ BEGIN IMPORTING relational_choice,
relational_choice_properties,
relation_implication END top_choice_facts
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.15Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
