Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: top_choice_facts.pvs Sprache: PVS

Original von: PVS^©

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

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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.