Independence of premise (original) (raw)
In proof theory and constructive mathematics, the principle of independence of premise states that if φ and ∃ x θ are sentences in a formal theory and φ → ∃ x θ is provable, then ∃ x (φ → θ) is provable. Here x cannot be a free variable of φ. The principle is valid in classical logic. Its main application is in the study of intuitionistic logic, where the principle is not always valid.
| Property | Value |
|---|---|
| dbo:abstract | In proof theory and constructive mathematics, the principle of independence of premise states that if φ and ∃ x θ are sentences in a formal theory and φ → ∃ x θ is provable, then ∃ x (φ → θ) is provable. Here x cannot be a free variable of φ. The principle is valid in classical logic. Its main application is in the study of intuitionistic logic, where the principle is not always valid. (en) Na teoria da prova e matemática construtiva, o princípio da independência de premissas afirma que, se φ e ∃ x θ são sentenças em uma teoria formal e φ → ∃ x θ é demonstrável, então ∃ x (φ → θ) é demonstrável. Neste caso x não pode ser uma variável livre de φ. A sua principal aplicação é no estudo da lógica intuicionística, onde o princípio nem sempre é válido. (pt) |
| dbo:wikiPageExternalLink | http://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf |
| dbo:wikiPageID | 22833480 (xsd:integer) |
| dbo:wikiPageLength | 2680 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1100424867 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:BHK_interpretation dbr:Free_variable dbr:Proof_theory dbc:Predicate_logic dbr:Law_of_the_excluded_middle dbr:Constructive_mathematics dbr:Weak_counterexample |
| dbp:wikiPageUsesTemplate | dbt:Cite_book |
| dct:subject | dbc:Predicate_logic |
| gold:hypernym | dbr:Sentences |
| rdfs:comment | In proof theory and constructive mathematics, the principle of independence of premise states that if φ and ∃ x θ are sentences in a formal theory and φ → ∃ x θ is provable, then ∃ x (φ → θ) is provable. Here x cannot be a free variable of φ. The principle is valid in classical logic. Its main application is in the study of intuitionistic logic, where the principle is not always valid. (en) Na teoria da prova e matemática construtiva, o princípio da independência de premissas afirma que, se φ e ∃ x θ são sentenças em uma teoria formal e φ → ∃ x θ é demonstrável, então ∃ x (φ → θ) é demonstrável. Neste caso x não pode ser uma variável livre de φ. A sua principal aplicação é no estudo da lógica intuicionística, onde o princípio nem sempre é válido. (pt) |
| rdfs:label | Independence of premise (en) Indepêndencia de premissas (pt) |
| owl:sameAs | freebase:Independence of premise wikidata:Independence of premise dbpedia-pt:Independence of premise https://global.dbpedia.org/id/4nb3i |
| prov:wasDerivedFrom | wikipedia-en:Independence_of_premise?oldid=1100424867&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Independence_of_premise |
| is dbo:wikiPageWikiLink of | dbr:Dialectica_interpretation |
| is foaf:primaryTopic of | wikipedia-en:Independence_of_premise |