860 lines
29 KiB
HTML
860 lines
29 KiB
HTML
<!DOCTYPE html>
|
||
<html lang='en'>
|
||
|
||
<head>
|
||
<meta charset='UTF-8' />
|
||
<meta name='viewport' content='width=device-width, initial-scale=1' />
|
||
<title>
|
||
Logik für Dummies – Home
|
||
</title>
|
||
|
||
|
||
<meta property='og:description' content='Logik ist das ziehen von Schlüssen, die innerhalb der Logik widerspruchsfrei und kohärent sind.' />
|
||
<meta property='og:site_name' content='Home' />
|
||
<meta property='og:image' content />
|
||
<meta property='og:type' content='website' />
|
||
<meta property='og:title' content='Logik für Dummies' />
|
||
|
||
|
||
<base href='/' />
|
||
<link href='favicon.svg' rel='icon' />
|
||
|
||
<script>
|
||
window.MathJax = {
|
||
startup: {
|
||
ready: () => {
|
||
MathJax.startup.defaultReady();
|
||
}
|
||
}
|
||
};
|
||
</script>
|
||
<script async id='MathJax-script' src='https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js'></script>
|
||
|
||
<!-- mermaid.js --><script src='https://cdn.jsdelivr.net/npm/mermaid/dist/mermaid.min.js'></script>
|
||
<script>
|
||
mermaid.initialize({startOnLoad:false});
|
||
mermaid.init(undefined,document.querySelectorAll(".mermaid"));
|
||
</script>
|
||
|
||
<!-- highlight.js -->
|
||
<link rel='stylesheet' href='https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.6.0/styles/hybrid.min.css' />
|
||
<script src='https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.6.0/highlight.min.js'></script>
|
||
<!-- Include languages that Emanote itself uses -->
|
||
<script src='https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.6.0/languages/haskell.min.js'></script>
|
||
<script src='https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.6.0/languages/nix.min.js'></script>
|
||
<script>hljs.highlightAll();</script>
|
||
|
||
|
||
|
||
|
||
<link href='tailwind.css?instanceId=ecadcd50-ecaf-4d6e-98ea-7932c3b3d351' rel='stylesheet' type='text/css' />
|
||
|
||
<!-- Heist error element -->
|
||
<style>
|
||
strong.error {
|
||
color: lightcoral;
|
||
font-size: 90%;
|
||
font-family: monospace;
|
||
}
|
||
</style>
|
||
<!-- What goes in this file will appear on near the end of <head>--><link rel='preload' href='_emanote-static/fonts/Maven_Pro/MavenPro-VariableFont_wght.ttf' as='font' type='font/ttf' crossorigin />
|
||
|
||
<style>
|
||
@font-face {
|
||
font-family: 'MavenPro';
|
||
/* FIXME: This ought to be: ${ema:emanoteStaticLayerUrl}/fonts/Maven_Pro/MavenPro-VariableFont_wght.ttf */
|
||
src: url(_emanote-static/fonts/Maven_Pro/MavenPro-VariableFont_wght.ttf) format("truetype");
|
||
font-display: swap;
|
||
}
|
||
|
||
body {
|
||
font-family: 'MavenPro', sans-serif;
|
||
/* font-variation-settings: 'wght'300; */
|
||
}
|
||
|
||
a.mavenLinkBold {
|
||
font-variation-settings: 'wght'500;
|
||
}
|
||
|
||
strong {
|
||
font-variation-settings: 'wght'500;
|
||
}
|
||
|
||
h1,
|
||
h2,
|
||
h3,
|
||
h4,
|
||
h5,
|
||
h6,
|
||
header,
|
||
.header-font {
|
||
font-family: 'MavenPro', sans-serif;
|
||
}
|
||
</style>
|
||
|
||
|
||
<link rel='stylesheet' href='_emanote-static/inverted-tree.css' />
|
||
|
||
<link rel='stylesheet' href='https://files.stork-search.net/releases/v1.5.0/flat.css' />
|
||
<!-- Custom Stork-search styling for Emanote -->
|
||
<style>
|
||
#stork-search-container {
|
||
z-index: 1000;
|
||
background-color: rgb(15 23 42/.8);
|
||
}
|
||
|
||
.stork-overflow-hidden-important {
|
||
overflow: hidden !important;
|
||
}
|
||
</style>
|
||
|
||
|
||
<script src='https://files.stork-search.net/releases/v1.5.0/stork.js'></script>
|
||
|
||
|
||
<script data-emanote-base-url='/'>
|
||
window.emanote = {};
|
||
window.emanote.stork = {
|
||
searchShown: false,
|
||
toggleSearch: function () {
|
||
document.getElementById('stork-search-container').classList.toggle('hidden');
|
||
window.emanote.stork.searchShown = document.body.classList.toggle('stork-overflow-hidden-important');
|
||
if (window.emanote.stork.searchShown) {
|
||
document.getElementById('stork-search-input').focus();
|
||
}
|
||
},
|
||
clearSearch: function () {
|
||
document.getElementById('stork-search-container').classList.add('hidden');
|
||
document.body.classList.remove('stork-overflow-hidden-important');
|
||
window.emanote.stork.searchShown = false;
|
||
},
|
||
|
||
init: function () {
|
||
const indexName = 'emanote-search'; // used to match input[data-stork] attribute value
|
||
const baseUrl = document.currentScript.getAttribute('data-emanote-base-url') || '/';
|
||
const indexUrl = baseUrl + '-/stork.st';
|
||
if (document.readyState !== 'complete') {
|
||
window.addEventListener('load', function () {
|
||
stork.register(indexName, indexUrl);
|
||
});
|
||
|
||
document.addEventListener('keydown', event => {
|
||
if (window.emanote.stork.searchShown && event.key === 'Escape') {
|
||
window.emanote.stork.clearSearch();
|
||
event.preventDefault();
|
||
} else if ((event.key == 'k' || event.key == 'K') && (event.ctrlKey || event.metaKey)) {
|
||
window.emanote.stork.toggleSearch();
|
||
event.preventDefault();
|
||
}
|
||
});
|
||
} else {
|
||
// Override existing on Ema's hot-reload
|
||
stork.register(indexName, indexUrl, { forceOverwrite: true });
|
||
}
|
||
}
|
||
};
|
||
|
||
window.emanote.stork.init();
|
||
</script>
|
||
|
||
|
||
</head>
|
||
|
||
<!-- DoNotFormat -->
|
||
|
||
|
||
|
||
<!-- DoNotFormat -->
|
||
|
||
<body class='bg-gray-400 overflow-y-scroll'>
|
||
|
||
<div class='container mx-auto'>
|
||
|
||
<nav id='breadcrumbs' class='w-full text-gray-700 md:hidden'>
|
||
<div class='flex justify-left'>
|
||
<div class='w-full px-2 py-2 bg-gray-50'>
|
||
<ul class='flex flex-wrap text-lg'>
|
||
<li class='inline-flex items-center'>
|
||
|
||
|
||
<img style='width: 1rem;' src='favicon.svg' />
|
||
|
||
|
||
</li>
|
||
|
||
|
||
<li class='inline-flex items-center'>
|
||
<a class='px-1 font-bold' href=''>
|
||
Home
|
||
</a>
|
||
<svg fill='currentColor' viewBox='0 0 20 20' class='w-auto h-5 text-gray-400'>
|
||
<path fill-rule='evenodd' d='M7.293 14.707a1 1 0 010-1.414L10.586 10 7.293 6.707a1 1 0 011.414-1.414l4 4a1 1 0 010 1.414l-4 4a1 1 0 01-1.414 0z' clip-rule='evenodd'></path>
|
||
</svg>
|
||
</li>
|
||
|
||
|
||
</ul>
|
||
</div>
|
||
<button class='inline px-2 py-1 bg-gray-50 outline-none cursor-pointer focus:outline-none' title='Search (Ctrl+K)' type='button' onclick='window.emanote.stork.toggleSearch()'>
|
||
<svg xmlns='http://www.w3.org/2000/svg' style='width: 1rem;' class='hover:text-purple-700' f
|
||
fill='none' viewBox='0 0 24 24' stroke='currentColor' stroke-width='2'>
|
||
<path stroke-linecap='round' stroke-linejoin='round' d='M21 21l-6-6m2-5a7 7 0 11-14 0 7 7 0 0114 0z'></path>
|
||
</svg>
|
||
</button>
|
||
<button class='inline px-2 py-1 text-white bg-purple-600 outline-none cursor-pointer focus:outline-none' title='Toggle sidebar' type='button' onclick="toggleHidden('sidebar')">
|
||
<svg xmlns='http://www.w3.org/2000/svg' class='w-4' fill='none' viewBox='0 0 24 24' stroke='currentColor'>
|
||
<path stroke-linecap='round' stroke-linejoin='round' stroke-width='2' d='M4 6h16M4 12h16M4 18h16'></path>
|
||
</svg>
|
||
</button>
|
||
<script>
|
||
function toggleHidden(elemId) {
|
||
document.getElementById(elemId).classList.toggle("hidden");
|
||
}
|
||
</script>
|
||
</div>
|
||
</nav>
|
||
|
||
<div id='container' class='flex flex-nowrap flex-col md:flex-row bg-gray-50 md:mt-8 md:shadow-2xl md:mb-8'>
|
||
<!-- Sidebar column -->
|
||
<nav id='sidebar' class='flex-shrink hidden leading-relaxed md:block md:sticky md:top-0 md:h-full md:w-48 xl:w-64'>
|
||
<div class='px-2 py-2 text-gray-800'>
|
||
<div id='indexing-links' class='flex flex-row float-right p-2 space-x-2 text-gray-500'>
|
||
<a href='-/tags' title='View tags'>
|
||
<svg style='width: 1rem;' class='hover:text-purple-700' fill='none' stroke='currentColor' viewBox='0 0 24 24' xmlns='http://www.w3.org/2000/svg'>
|
||
<path stroke-linecap='round' stroke-linejoin='round' stroke-width='2' d='M7 7h.01M7 3h5c.512 0 1.024.195 1.414.586l7 7a2 2 0 010 2.828l-7 7a2 2 0 01-2.828 0l-7-7A1.994 1.994 0 013 12V7a4 4 0 014-4z'>
|
||
</path>
|
||
</svg>
|
||
</a>
|
||
<a href='-/all' title='Expand full tree'>
|
||
<svg style='width: 1rem;' class='hover:text-purple-700' fill='none' stroke='currentColor' viewBox='0 0 24 24' xmlns='http://www.w3.org/2000/svg'>
|
||
<path stroke-linecap='round' stroke-linejoin='round' stroke-width='2' d='M4 8V4m0 0h4M4 4l5 5m11-1V4m0 0h-4m4 0l-5 5M4 16v4m0 0h4m-4 0l5-5m11 5l-5-5m5 5v-4m0 4h-4'>
|
||
</path>
|
||
</svg>
|
||
</a>
|
||
<a title='Search (Ctrl+K)' class='cursor-pointer' onclick='window.emanote.stork.toggleSearch()'>
|
||
<svg xmlns='http://www.w3.org/2000/svg' style='width: 1rem;' class='hover:text-purple-700' f
|
||
fill='none' viewBox='0 0 24 24' stroke='currentColor' stroke-width='2'>
|
||
<path stroke-linecap='round' stroke-linejoin='round' d='M21 21l-6-6m2-5a7 7 0 11-14 0 7 7 0 0114 0z'></path>
|
||
</svg>
|
||
</a>
|
||
</div>
|
||
|
||
<div id='site-logo' class='pl-2'>
|
||
<div class='flex items-center my-2 space-x-2 justify-left'>
|
||
<a href='' title='Go to Home'>
|
||
|
||
|
||
<!-- The style width attribute here is to prevent huge
|
||
icon from displaying at those rare occasions when Tailwind
|
||
hasn't kicked in immediately on page load
|
||
-->
|
||
<img style='width: 1rem;' class='transition transform hover:scale-110 hover:opacity-80' src='favicon.svg' />
|
||
|
||
|
||
</a>
|
||
<a class='font-bold truncate' title='Go to Home' href=''>
|
||
Home
|
||
</a>
|
||
</div>
|
||
</div>
|
||
|
||
|
||
<!-- Variable bindings for this tree-->
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
<!-- Rendering of this tree -->
|
||
<div class='pl-2'>
|
||
<!-- Node's rootLabel-->
|
||
<div class='flex items-center my-2 space-x-2 justify-left'>
|
||
|
||
|
||
<svg xmlns='http://www.w3.org/2000/svg' class='w-4 h-4 flex-shrink-0 inline text-gray-500' viewBox='0 0 20 20' fill='currentColor'>
|
||
<path d='M2 6a2 2 0 012-2h5l2 2h5a2 2 0 012 2v6a2 2 0 01-2 2H4a2 2 0 01-2-2V6z'></path>
|
||
</svg>
|
||
|
||
|
||
<a class='hover:underline truncate' title='About' href='About'>
|
||
About
|
||
</a>
|
||
|
||
|
||
<span class='text-gray-300' title='3 children inside'>
|
||
3
|
||
</span>
|
||
|
||
|
||
</div>
|
||
|
||
<!-- Node's children forest, displayed only on active trees
|
||
TODO: Use <details> to toggle visibility?
|
||
-->
|
||
|
||
</div>
|
||
|
||
<!-- Variable bindings for this tree-->
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
<!-- Rendering of this tree -->
|
||
<div class='pl-2'>
|
||
<!-- Node's rootLabel-->
|
||
<div class='flex items-center my-2 space-x-2 justify-left'>
|
||
|
||
|
||
<svg xmlns='http://www.w3.org/2000/svg' class='w-4 h-4 flex-shrink-0 inline text-gray-500' viewBox='0 0 20 20' fill='currentColor'>
|
||
<path d='M2 6a2 2 0 012-2h5l2 2h5a2 2 0 012 2v6a2 2 0 01-2 2H4a2 2 0 01-2-2V6z'></path>
|
||
</svg>
|
||
|
||
|
||
<a class='hover:underline truncate' title='Android' href='Android'>
|
||
Android
|
||
</a>
|
||
|
||
|
||
<span class='text-gray-300' title='1 children inside'>
|
||
1
|
||
</span>
|
||
|
||
|
||
</div>
|
||
|
||
<!-- Node's children forest, displayed only on active trees
|
||
TODO: Use <details> to toggle visibility?
|
||
-->
|
||
|
||
</div>
|
||
|
||
<!-- Variable bindings for this tree-->
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
<!-- Rendering of this tree -->
|
||
<div class='pl-2'>
|
||
<!-- Node's rootLabel-->
|
||
<div class='flex items-center my-2 space-x-2 justify-left'>
|
||
|
||
|
||
<svg xmlns='http://www.w3.org/2000/svg' class='w-4 h-4 flex-shrink-0 inline text-gray-500' viewBox='0 0 20 20' fill='currentColor'>
|
||
<path d='M2 6a2 2 0 012-2h5l2 2h5a2 2 0 012 2v6a2 2 0 01-2 2H4a2 2 0 01-2-2V6z'></path>
|
||
</svg>
|
||
|
||
|
||
<a class='hover:underline truncate' title='Haskell' href='Haskell'>
|
||
Haskell
|
||
</a>
|
||
|
||
|
||
<span class='text-gray-300' title='5 children inside'>
|
||
5
|
||
</span>
|
||
|
||
|
||
</div>
|
||
|
||
<!-- Node's children forest, displayed only on active trees
|
||
TODO: Use <details> to toggle visibility?
|
||
-->
|
||
|
||
</div>
|
||
|
||
<!-- Variable bindings for this tree-->
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
<!-- Rendering of this tree -->
|
||
<div class='pl-2'>
|
||
<!-- Node's rootLabel-->
|
||
<div class='flex items-center my-2 space-x-2 justify-left'>
|
||
|
||
|
||
<svg class='w-4 h-4 flex-shrink-0 inline' fill='none' stroke='currentColor' viewBox='0 0 24 24' xmlns='http://www.w3.org/2000/svg'>
|
||
<path stroke-linecap='round' stroke-linejoin='round' stroke-width='2' d='M9 12h6m-6 4h6m2 5H7a2 2 0 01-2-2V5a2 2 0 012-2h5.586a1 1 0 01.707.293l5.414 5.414a1 1 0 01.293.707V19a2 2 0 01-2 2z'>
|
||
</path>
|
||
</svg>
|
||
|
||
|
||
<a class='font-bold text-purple-600 hover:underline truncate' title='Logik für Dummies' href='Logik'>
|
||
Logik für Dummies
|
||
</a>
|
||
|
||
|
||
</div>
|
||
|
||
<!-- Node's children forest, displayed only on active trees
|
||
TODO: Use <details> to toggle visibility?
|
||
-->
|
||
|
||
|
||
|
||
</div>
|
||
|
||
<!-- Variable bindings for this tree-->
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
<!-- Rendering of this tree -->
|
||
<div class='pl-2'>
|
||
<!-- Node's rootLabel-->
|
||
<div class='flex items-center my-2 space-x-2 justify-left'>
|
||
|
||
|
||
<svg xmlns='http://www.w3.org/2000/svg' class='w-4 h-4 flex-shrink-0 inline text-gray-500' viewBox='0 0 20 20' fill='currentColor'>
|
||
<path d='M2 6a2 2 0 012-2h5l2 2h5a2 2 0 012 2v6a2 2 0 01-2 2H4a2 2 0 01-2-2V6z'></path>
|
||
</svg>
|
||
|
||
|
||
<a class='hover:underline truncate' title='Uni' href='Uni'>
|
||
Uni
|
||
</a>
|
||
|
||
|
||
<span class='text-gray-300' title='2 children inside'>
|
||
2
|
||
</span>
|
||
|
||
|
||
</div>
|
||
|
||
<!-- Node's children forest, displayed only on active trees
|
||
TODO: Use <details> to toggle visibility?
|
||
-->
|
||
|
||
</div>
|
||
|
||
<!-- Variable bindings for this tree-->
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
<!-- Rendering of this tree -->
|
||
<div class='pl-2'>
|
||
<!-- Node's rootLabel-->
|
||
<div class='flex items-center my-2 space-x-2 justify-left'>
|
||
|
||
|
||
<svg xmlns='http://www.w3.org/2000/svg' class='w-4 h-4 flex-shrink-0 inline text-gray-500' viewBox='0 0 20 20' fill='currentColor'>
|
||
<path d='M2 6a2 2 0 012-2h5l2 2h5a2 2 0 012 2v6a2 2 0 01-2 2H4a2 2 0 01-2-2V6z'></path>
|
||
</svg>
|
||
|
||
|
||
<a class='hover:underline truncate' title='Unix' href='Unix'>
|
||
Unix
|
||
</a>
|
||
|
||
|
||
<span class='text-gray-300' title='1 children inside'>
|
||
1
|
||
</span>
|
||
|
||
|
||
</div>
|
||
|
||
<!-- Node's children forest, displayed only on active trees
|
||
TODO: Use <details> to toggle visibility?
|
||
-->
|
||
|
||
</div>
|
||
|
||
|
||
</div>
|
||
</nav>
|
||
|
||
<!-- Main body column -->
|
||
<div class='flex-1 w-full overflow-x-auto bg-white'>
|
||
<main class='px-4 py-4'>
|
||
<!-- DoNotFormat -->
|
||
<!-- DoNotFormat -->
|
||
|
||
<nav id='uptree' class='flipped tree' style='transform-origin: 50%;'>
|
||
<ul class='root'>
|
||
<li>
|
||
|
||
<ul>
|
||
|
||
<li>
|
||
|
||
<div class='text-gray-900 forest-link'>
|
||
<a href=''>
|
||
Home
|
||
</a>
|
||
</div>
|
||
|
||
|
||
</li>
|
||
|
||
</ul>
|
||
|
||
</li>
|
||
</ul>
|
||
</nav>
|
||
<h1 class='flex items-end justify-center mb-4 p-3 bg-purple-100 text-5xl font-extrabold text-black rounded'>
|
||
<a class='z-40 tracking-tighter '>
|
||
Logik für Dummies
|
||
</a>
|
||
</h1>
|
||
<article class='overflow-auto'>
|
||
<!-- What goes in this file will appear on top of note body-->
|
||
|
||
<p class='mb-3'>
|
||
Logik ist das ziehen von Schlüssen, die innerhalb der Logik widerspruchsfrei und kohärent sind.
|
||
</p>
|
||
<h1 id='minimale-logik' class='pb-2 mb-2 text-5xl font-bold text-center'>minimale Logik</h1>
|
||
<p class='mb-3'>
|
||
Für eine minimale Logik braucht man folgende Annahmen:
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Im folgenden ist jedes Merkmal als Dreiklang definiert, bestehend aus einer Formaldefinition (F - WAS ist das), einer Einführung (I - WIE kann ich das “erzeugen”) und einer Elimination (E - WIE bekomme ich das wieder weg).
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Formal kurz:
|
||
</p>
|
||
|
||
<ul class='my-3 ml-6 space-y-1 list-disc'>
|
||
|
||
<li>
|
||
prop ist eine Eigenschaft, die zu true oder false evaluieren kann. Wir berüchsichtigen nur ein weiteres schließen, wenn prop entweder wahr oder unevaluiert ist.
|
||
</li>
|
||
|
||
<li>
|
||
A, B, C sind Aussagen
|
||
</li>
|
||
|
||
<li>
|
||
<span class='math inline'>\(\Gamma\)</span> sind Aussagensammlungen (eine beliebige Anzahl an Aussagen in beliebiger Reihenfolge)
|
||
</li>
|
||
|
||
</ul>
|
||
|
||
<p class='mb-3'>
|
||
Alle weiteren Operationen werden eingeführt.
|
||
</p>
|
||
<h2 id='wahrheit-t' class='inline-block mt-6 mb-4 text-4xl font-bold text-gray-700 border-b-2'>Wahrheit T</h2>
|
||
<p class='mb-3'>
|
||
Eine Wahrheit T, auf die jede Aussage die logisch ist reduzierbar sein muss:
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{}{T prop} (T-F)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
“prop” ist einfach eine Aussage.
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{}{T true} (T-I)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Es gibt keine “ultimative” Wahrheit, aus der ich trivial “wahr” ableiten kann. Normalerweise bekannt als “Axiome”. Später einfach Grundannahmen.
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(- (T-E)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Es gibt keine Elimination. Etwas, was inherent Wahr ist, kann ich nicht im Nachhinein ändern (ohne zuvor einen Fehler gemacht zu haben).
|
||
</p>
|
||
<h2 id='verknüpfung-wedge' class='inline-block mt-6 mb-4 text-4xl font-bold text-gray-700 border-b-2'>Verknüpfung <span class='math inline'>\(\wedge\)</span></h2>
|
||
<p class='mb-3'>
|
||
Eine Verknüpfung <span class='math inline'>\(\wedge\)</span>, die zutrifft, wenn 2 Aussagen A, B wahr sind:
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{A prop; B prop}{A \wedge B prop} (\wedge F)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
A & B sind Aussagen, Ergebnis ist eine Aussage über beides
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{A true; B true}{A \wedge B true} (\wedge I)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Wenn A wahr & B wahr, dann ist beides zusammen auch wahr.
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{A \wedge B true}{A true} (\wedge E_1)\quad \frac{A \wedge B true}{B true} (\wedge E_2)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Wenn A & B wahr sind, dann auch die Teile
|
||
</p>
|
||
<h2 id='implikation-supset' class='inline-block mt-6 mb-4 text-4xl font-bold text-gray-700 border-b-2'>Implikation <span class='math inline'>\(\supset\)</span></h2>
|
||
<p class='mb-3'>
|
||
Eine Implikation (B ist in A enthalten):
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{A prop; B prop}{A \supset B prop} (\supset F)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
A & B sind Aussagen, Ergebnis ist eine Aussage über beides
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{A true \vdash B true}{A \supset B true} (\supset I)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Wenn A B impliziert, dann ist A eine größere Aussage als B.
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{A \supset B true; A true}{B true} (\supset E)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Wenn A B umfasst und A wahr ist, dann muss B wahr sein.
|
||
</p>
|
||
<h2 id='entailment-vdash' class='inline-block mt-6 mb-4 text-4xl font-bold text-gray-700 border-b-2'>Entailment <span class='math inline'>\(\vdash\)</span></h2>
|
||
<p class='mb-3'>
|
||
Was soll nun dieser <span class='math inline'>\(\vdash\)</span>-Operator sein? Nun, dass ist “folgerbarkeit”. Folgende Bedingungen <strong>müssen</strong> erfüllt sein, damit das (für uns) sinnvoll ist:
|
||
</p>
|
||
|
||
<ul class='my-3 ml-6 space-y-1 list-decimal list-inside'>
|
||
|
||
<li>
|
||
<span class='math inline'>\(A true \vdash A true\)</span> (Reflexiv, Wenn A wahr ist, dann folgt daraus, dass A wahr ist!)
|
||
</li>
|
||
|
||
<li>
|
||
<span class='math inline'>\(\frac{\Gamma_1 \vdash A true; \Gamma_2, A true \vdash B true}{\Gamma_1, \Gamma_2 \vdash B true}\)</span> (Transitiv, Wenn A unter Bedingung X wahr ist, und B unter Bedingung AY, dann ist B auch unter XY wahr. Wenn 1 + 1 = 2 und 3+2 = 5, dann auch 3 + (1+1) = 5)
|
||
</li>
|
||
|
||
</ul>
|
||
|
||
<p class='mb-3'>
|
||
und folgendes <strong>sollte</strong> erfüllt sein, außer wir bewegen uns auf ganz krudem Terrain:
|
||
</p>
|
||
|
||
<ul class='my-3 ml-6 space-y-1 list-decimal list-inside'>
|
||
|
||
<li>
|
||
<span class='math inline'>\(\frac{\Gamma \vdash A true}{\Gamma, B true \vdash A true}\)</span> (Weakening. Wenn A schon bewiesen ist, dann wird es nicht falsch durch hinzufügen einer wahren Vorraussetzung (die für den Beweis nicht nötig wäre)).
|
||
</li>
|
||
|
||
<li>
|
||
<span class='math inline'>\(\frac{\Gamma, A true, A true \vdash B true}{\Gamma, A true \vdash B true}\)</span> (Contraction. Wenn ich A 2x verwende, dann kann ich es auch nur 1x oben drüber schreiben).
|
||
</li>
|
||
|
||
<li>
|
||
<span class='math inline'>\(\frac{\Gamma \vdash A true}{\Pi(\Gamma) A true}\)</span> (Permutation. Egal in welcher Permutation <span class='math inline'>\(\pi\)</span> ich die Argumente aufführe, der Schluss ist gleich).
|
||
</li>
|
||
|
||
</ul>
|
||
<h2 id='unwahrheit-perp' class='inline-block mt-6 mb-4 text-4xl font-bold text-gray-700 border-b-2'>Unwahrheit <span class='math inline'>\(\perp\)</span></h2>
|
||
<p class='mb-3'>
|
||
Eine Aussage, die <strong>nie</strong> Eintreten darf. Wenn wird dieses Schlussfolgern <em>können</em>, dann haben wir einen Fehler
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{}{\perp prop} (\perp F)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
bottom ist eine Aussage
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(-(\perp I)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
bottom kann nicht Abgeleitet werden
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{\perp true}{A true} (\perp E)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Wenn wir bottom Ableiten können, gilt alles (1=0, Gott existiert und existiert nicht zugleich, …).
|
||
</p>
|
||
<h2 id='disjunktion-vee' class='inline-block mt-6 mb-4 text-4xl font-bold text-gray-700 border-b-2'>Disjunktion <span class='math inline'>\(\vee\)</span></h2>
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{A prop, B prop}{A \vee B prop} (\vee F)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
A & B sind Aussagen, A oder B ist auch eine Aussage
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{A true}{A \vee B true} (\vee I_1)\quad \frac{B true}{A \vee B true} (\vee I_2)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Wenn eins von beidem Wahr ist, dann ist A oder B wahr. Sprich, ich kann einfach irgendeine Aussage (egal ob wahr oder falsch) zu einer Aussage hinzufügen und die Disjunktion bleibt gleich.
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
<span class='math inline'>\(\frac{A \vee B true, A true \vdash C true, B true \vdash C true}{C true} (\vee E)\)</span>
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Wenn C aus A folgt UND C aus B folgt UND entweder A oder B wahr sind, ist C wahr. OB jetzt entweder A oder B wahr sind interessiert für den Schluss nicht. Es reicht, dass Eines von beiden wahr ist.
|
||
</p>
|
||
<h1 id='folgerungen' class='pb-2 mb-2 text-5xl font-bold text-center'>Folgerungen</h1>
|
||
<ul class='my-3 ml-6 space-y-1 list-decimal list-inside'>
|
||
|
||
<li>
|
||
Eine Aussage A ist immer <span class='math inline'>\(\perp \le A \le T\)</span>. Sie ist also wahr oder falsch (=trivial) oder je nach Bedingung anders.
|
||
</li>
|
||
|
||
<li>
|
||
Es gibt eine “Mächtigkeitsreihenfolge” bei Aussagen. Die Aussagen, die mit den wenigsten Vorraussetzungen auskommen sind mächtiger und enthalten mehr Aussagen, als die speziellen.
|
||
</li>
|
||
|
||
<li>
|
||
Zu einer Aussage A gibt es eine Gegenaussage <span class='math inline'>\(\neg A := A \supset \perp\)</span>. Diese ist genau dann falsch, wenn A wahr ist. Formal: <span class='math inline'>\(\frac{A \wedge C \le \perp }{C \le \neg A}\)</span>. Wenn A widerlegt werden kann, ist <span class='math inline'>\(\neg A\)</span> die mächtigste Widerlegung.
|
||
</li>
|
||
|
||
<li>
|
||
Zu einer Aussage A gibt es ein Inverses <span class='math inline'>\(\bar{A}\)</span>, sodass <span class='math inline'>\(A \vee \bar{A} \simeq T\)</span>, also <span class='math inline'>\(T \le A \vee \bar{A}\)</span>. <span class='math inline'>\(\bar{A}\)</span> ist somit die größte Aussage, die dazu führt, dass sie mit A ver-odert wahr wird.
|
||
</li>
|
||
|
||
<li>
|
||
<strong>Bemerkenswert ist:</strong> Im Allgemeinen gilt <em>nicht</em>: <span class='math inline'>\(\neg A = \bar{A}\)</span>.
|
||
</li>
|
||
|
||
</ul>
|
||
|
||
<p class='mb-3'>
|
||
Zu 5. noch eine Bemerkung: Dies ist trivial klar, wenn man sich bewusst macht, dass nicht jedes Problem gelöst ist. Dies sind Dinge, über die die Logik alleine keine Aussage treffen KANN. Allerdings müssen wir Berücksichtigen, dass es solche Annahmen GIBT.
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Ein Beispiel für eine Logik, die Annahme 5 macht: Bool’sche Algebra
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Ein Beispiel für eine Logik, die Annahme 5 <em>nicht</em> macht: Heyting Algebra, u.U. auch Lindenbaum Algebra (nicht geprüft)
|
||
</p>
|
||
|
||
<p class='mb-3'>
|
||
Damit ist letztere qua definitionem mächtiger als Erstgenannte, da diese in letztgenannter enthalten ist.
|
||
</p>
|
||
|
||
<!-- div class="flex items-center justify-center mt-2">
|
||
<ema:metadata>
|
||
<with var="template">
|
||
<a class="text-gray-300 hover:text-${theme}-600 text-sm" title="Edit this page on GitHub"
|
||
href="${value:editBaseUrl}/${ema:note:source-path}">
|
||
<svg xmlns="http://www.w3.org/2000/svg" class="h-6 w-6" fill="none" viewBox="0 0 24 24" stroke="currentColor">
|
||
<path stroke-linecap="round" stroke-linejoin="round" stroke-width="2"
|
||
d="M11 5H6a2 2 0 00-2 2v11a2 2 0 002 2h11a2 2 0 002-2v-5m-1.414-9.414a2 2 0 112.828 2.828L11.828 15H9v-2.828l8.586-8.586z" />
|
||
</svg>
|
||
</a>
|
||
</with>
|
||
</ema:metadata>
|
||
</div -->
|
||
</article>
|
||
<div class='flex flex-col lg:flex-row lg:space-x-2'>
|
||
|
||
|
||
</div>
|
||
|
||
<section class='flex flex-wrap items-end justify-center my-4 space-x-2 space-y-2 font-mono text-sm'>
|
||
|
||
</section>
|
||
|
||
<!-- What goes in this file will at the very end of the main div -->
|
||
</main>
|
||
</div>
|
||
</div>
|
||
<footer class='flex items-center justify-center mt-2 mb-8 space-x-4 text-center text-gray-800'>
|
||
|
||
<div>
|
||
<a href='' title='Go to Home page'>
|
||
<svg xmlns='http://www.w3.org/2000/svg' class='w-6 h-6 hover:text-purple-700' fill='none' viewBox='0 0 24 24' stroke='currentColor'>
|
||
<path stroke-linecap='round' stroke-linejoin='round' stroke-width='2' d='M3 12l2-2m0 0l7-7 7 7M5 10v10a1 1 0 001 1h3m10-11l2 2m-2-2v10a1 1 0 01-1 1h-3m-6 0a1 1 0 001-1v-4a1 1 0 011-1h2a1 1 0 011 1v4a1 1 0 001 1m-6 0h6'></path>
|
||
</svg>
|
||
</a>
|
||
</div>
|
||
<div>
|
||
<a href='-/all' title='View Index'>
|
||
<svg class='w-6 h-6 hover:text-purple-700' fill='none' stroke='currentColor' viewBox='0 0 24 24' xmlns='http://www.w3.org/2000/svg'>
|
||
<path stroke-linecap='round' stroke-linejoin='round' stroke-width='2' d='M4 8V4m0 0h4M4 4l5 5m11-1V4m0 0h-4m4 0l-5 5M4 16v4m0 0h4m-4 0l5-5m11 5l-5-5m5 5v-4m0 4h-4'>
|
||
</path>
|
||
</svg>
|
||
</a>
|
||
</div>
|
||
<div>
|
||
<a href='https://emanote.srid.ca' target='_blank' title='Generated by Emanote 0.7.3.0'>
|
||
<img class='w-6 h-6 hover:text-purple-700' src='_emanote-static/emanote-logo.svg' />
|
||
</a>
|
||
</div>
|
||
<div>
|
||
<a href='-/tags' title='View tags'>
|
||
<svg class='w-6 h-6 hover:text-purple-700' fill='none' stroke='currentColor' viewBox='0 0 24 24' xmlns='http://www.w3.org/2000/svg'>
|
||
<path stroke-linecap='round' stroke-linejoin='round' stroke-width='2' d='M7 7h.01M7 3h5c.512 0 1.024.195 1.414.586l7 7a2 2 0 010 2.828l-7 7a2 2 0 01-2.828 0l-7-7A1.994 1.994 0 013 12V7a4 4 0 014-4z'>
|
||
</path>
|
||
</svg>
|
||
</a>
|
||
</div>
|
||
<div>
|
||
<a href='-/tasks' title='View tasks'>
|
||
<svg xmlns='http://www.w3.org/2000/svg' class='w-6 h-6 hover:text-purple-700' fill='none' viewBox='0 0 24 24' stroke='currentColor'>
|
||
<path stroke-linecap='round' stroke-linejoin='round' stroke-width='2' d='M9 12l2 2 4-4m6 2a9 9 0 11-18 0 9 9 0 0118 0z'></path>
|
||
</svg>
|
||
</a>
|
||
</div>
|
||
</footer>
|
||
</div>
|
||
|
||
<div id='stork-search-container' class='hidden fixed w-screen h-screen inset-0 backdrop-filter backdrop-blur-sm'>
|
||
<div class='fixed w-screen h-screen inset-0' onclick='window.emanote.stork.toggleSearch()'></div>
|
||
|
||
<div class='container mx-auto p-10 mt-10'>
|
||
<div class='stork-wrapper-flat container mx-auto'>
|
||
<input id='stork-search-input' data-stork='emanote-search' class='stork-input' placeholder='Search (Ctrl+K) ...' />
|
||
<div data-stork='emanote-search-output' class='stork-output'></div>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</body>
|
||
|
||
</html>
|